Superposition Reasoning about Quantified Bitvector Formulas

descriptionPublicationkeyboard_double_arrow_right Article , Conference object 01 Sep 2019Embargo end date: 26 Nov 2020Publisher:IEEEJournal:2019 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)Funded by:EC | SYMCAR, EC | AI4REASON, EC | SYMELS

Authors: David Damestani; Laura Kovács; Martin Suda 0001;

doi: 10.1109/synasc49474.2019.00022 , 10.34726/342

Superposition Reasoning about Quantified Bitvector Formulas

- Summary
- Subjects
- Metrics

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.

Related Organizations

TU Wien
Austria
Czech Technical University in Prague
Czech Republic
University of Vienna
Austria

Keywords

formal methods, SMT, bitvectors, automated reasoning, heorem proving

Impact byBIP!

	selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	0
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average