| 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 | Size | Format | Existing users please Login |
|---|---|---|---|---|
| S36_revised.pdf | accepted version | 226.41 kB | Adobe PDF | Embargoed until March 30, 2022 Request a copy |
Google ScholarTM
Check
Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.