<div class="csl-bib-body">
<div class="csl-entry">Damestani, D., Kovacs, L., & Suda, M. (2020). Superposition Reasoning about Quantified Bitvector Formulas. In H. Hong, V. Negru, D. Petcu, & D. Zaharie (Eds.), <i>Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing</i> (pp. 95–99). IEEE. https://doi.org/10.34726/342</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/16309
-
dc.identifier.uri
https://doi.org/10.34726/342
-
dc.description.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.
en
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.description.sponsorship
European Commission
-
dc.description.sponsorship
European Commission
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
formal methods
en
dc.subject
automated reasoning
en
dc.subject
heorem proving
en
dc.subject
SMT
en
dc.subject
bitvectors
en
dc.title
Superposition Reasoning about Quantified Bitvector Formulas
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Urheberrechtsschutz
de
dc.rights.license
In Copyright
en
dc.identifier.doi
10.34726/342
-
dc.contributor.affiliation
North Carolina State University, USA
-
dc.contributor.affiliation
West University of Timisoara, Romania
-
dc.contributor.editoraffiliation
North Carolina State University, USA
-
dc.contributor.editoraffiliation
West University of Timisoara, Romania
-
dc.contributor.editoraffiliation
West University of Timisoara, Romania
-
dc.contributor.editoraffiliation
West University of Timisoara, Romania
-
dc.relation.isbn
978-1-7281-5724-5
-
dc.relation.doi
10.1109/SYNASC49474.2019
-
dc.description.startpage
95
-
dc.description.endpage
99
-
dc.relation.grantno
S11412-N23
-
dc.relation.grantno
639270
-
dc.relation.grantno
842066
-
dcterms.dateSubmitted
2019-09
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
-
tuw.peerreviewed
true
-
tuw.relation.publisher
IEEE
-
tuw.version
am
-
tuw.project.title
Probabilistic Analysis of Distributed Systems
-
tuw.project.title
Symbolic Computation and Automated Reasoning for Program Analysis
-
tuw.project.title
Symbol Elimination in Reliable System Engineering
-
tuw.linking
https://ieeexplore.ieee.org/document/9049847
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.publisher.doi
10.1109/SYNASC49474.2019.00022
-
dc.description.numberOfPages
5
-
tuw.author.orcid
0000-0002-8299-2714
-
dc.rights.identifier
Urheberrechtsschutz
de
dc.rights.identifier
In Copyright
en
dc.description.sponsorshipexternal
European Commission
-
dc.description.sponsorshipexternal
KAW Foundation
-
dc.relation.grantnoexternal
649043
-
dc.relation.grantnoexternal
Wallenberg Academy Fellowship 2014
-
item.cerifentitytype
Publications
-
item.openaccessfulltext
Open Access
-
item.fulltext
with Fulltext
-
item.languageiso639-1
en
-
item.grantfulltext
open
-
item.openairetype
conference paper
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.mimetype
application/pdf
-
crisitem.author.dept
North Carolina State University, USA
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
