Title: Superposition Reasoning about Quantified Bitvector Formulas
Authors: Damestani, David 
Kovacs, Laura 
Suda, Martin 
Petcu, Dana 
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.
URI: http://hdl.handle.net/20.500.12708/16309
http://dx.doi.org/10.34726/342
DOI: 10.34726/342
Organisation: E192-04 - Forschungsbereich Formal Methods in Systems Engineering 
License: Urheberrechtsschutz 1.0
Publication Type: Inproceedings
Konferenzbeitrag
Appears in Collections:Conference Paper

Files in this item:

File Description SizeFormat Existing users please Login
S36_revised.pdfaccepted version226.41 kBAdobe PDFEmbargoed until March 30, 2022    Request a copy
Show full item record

Google ScholarTM

Check


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.