Record link: 
http://hdl.handle.net/20.500.12708/16309
http://dx.doi.org/10.34726/342
-
Title: 
Superposition Reasoning about Quantified Bitvector Formulas
en
Citation: 
Damestani, D., Kovacs, L., & Suda, M. (2020). Superposition Reasoning about Quantified Bitvector Formulas. In H. Hong, V. Negru, D. Petcu, & D. Zaharie (Eds.), Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (pp. 95–99). IEEE. https://doi.org/10.34726/342
-
reposiTUm DOI: 
10.34726/342
-
Publisher DOI: 
10.1109/SYNASC49474.2019.00022
-
Publication Type: 
Inproceedings - Full-Paper Contribution
en
 
Konferenzbeitrag - Full-Paper Contribution
de
Language: 
English
-
Authors: 
Damestani, David 
Kovacs, Laura 
Suda, Martin 
-
Organisational Unit: 
E192-04 - Forschungsbereich Formal Methods in Systems Engineering 
-
Published in: 
Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing 
-
ISBN: 
978-1-7281-5724-5
-
DOI of the book: 
10.1109/SYNASC49474.2019
-
Date (published): 
15-Apr-2020
-
Number of Pages: 
5
-
Publisher: 
IEEE
-
Peer reviewed: 
Yes
-
Keywords: 
formal methods; automated reasoning; heorem proving; SMT; bitvectors
en
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
Project title: 
RiSE/SHiNE 
Symbolic Computation and Automated Reasoning for Program Analysis 
Symbol Elimination in Reliable System Engineering 
-
Project ID: 
S11409-N23
639270
842066
-
Funder: 
Austrian FWF grant
European Commission
European Commission
-
Project (external): 
European Commission
KAW Foundation
-
Project ID: 
649043
Wallenberg Academy Fellowship 2014
-
Link (external): 
https://ieeexplore.ieee.org/document/9049847
-
License: 
In Copyright 1.0
en
Appears in Collections:
Conference Paper

Fulltext (Accepted Version)
Adobe PDF
(226.41 kB)
accepted version
Open Access In Copyright 1.0
Show full item record

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

Page view(s)

172
checked on Jan 25, 2023

Download(s)

44
checked on Jan 25, 2023

Google ScholarTM

Check