Superposition Reasoning about Quantified Bitvector Formulas

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F19%3A00346744" target="_blank" >RIV/68407700:21730/19:00346744 - isvavai.cz</a>

Result on the web

<a href="https://doi.org/10.1109/SYNASC49474.2019.00022" target="_blank" >https://doi.org/10.1109/SYNASC49474.2019.00022</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1109/SYNASC49474.2019.00022" target="_blank" >10.1109/SYNASC49474.2019.00022</a>

Result language

angličtina

Original language name

Superposition Reasoning about Quantified Bitvector Formulas

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

—

Continuities

R - Projekt Ramcoveho programu EK

Publication year

2019

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

2019 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)

ISBN

978-1-7281-5724-5

ISSN

—

e-ISSN

—

Number of pages

5

Pages from-to

95-99

Publisher name

IEEE Industrial Electronic Society

Place of publication

Vienna

Event location

Timisoara

Event date

Sep 4, 2019

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—