|Title:||Superposition Reasoning about Quantified Bitvector Formulas||Authors:||Damestani, David
|Keywords:||formal methods; automated reasoning; heorem proving; SMT; bitvectors||Issue Date:||15-Apr-2020||Book Title:||Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing||Abstract:||
We describe recent extensions to the first-order
theorem prover Vampire for proving theorems in the theory
of fixed-sized bitvectors, possibly with quantifiers. Details are
given on extending both the parser of Vampire as well as
the theory reasoning framework of Vampire. We present
our experimental results by evaluating and comparing our
approach to SMT solvers. Our experiments report also on a
few examples that can be solved only by our work.
|DOI:||10.34726/342||Organisation:||E192-04 - Forschungsbereich Formal Methods in Systems Engineering||License:||Urheberrechtsschutz 1.0||Publication Type:||Inproceedings
|Appears in Collections:||Conference Paper|
Show full item record
Files in this item:
Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.