<div class="csl-bib-body">
<div class="csl-entry">Damestani, D. (2020). <i>Superposition reasoning about quantied bitvector formulas</i> [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2023.77502</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2023.77502
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/188232
-
dc.description.abstract
Wir beschreiben die Erweiterungen des Theorembeweisers in Logik erster Ordnung Vampire, um Theoreme in der Theorie der Bitvektoren fester Größe zu beweisen, möglicherweise mit Quantoren. Es werden sowohl Details zur Erweiterung des Parsers von Vampire als auch des Argumentationsverfahren von Vampire gegeben. Wir präsentieren unsere experimentellen Ergebnisse, indem wir unseren Ansatz mit SMT-Löser vergleichen und evaluiren. Unsere Experimente berichten auch über einige Beispiele, die nur durch unseren Arbeit bewiesen werden können.
de
dc.description.abstract
We describe 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.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
automate reasoning
en
dc.subject
quantified bitvectors
en
dc.subject
memory reasoning
en
dc.subject
first-order theorem proving
en
dc.title
Superposition reasoning about quantied bitvector formulas
