Superposition Reasoning about Quantified Bitvector Formulas

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Superposition Reasoning about Quantified Bitvector Formulas

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Superposition Reasoning about Quantified Bitvector Formulas

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

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

Projekt

—

Návaznosti

R - Projekt Ramcoveho programu EK

Rok uplatnění

2019

Kód důvěrnosti údajů

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

Název statě ve sborníku

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

ISBN

978-1-7281-5724-5

ISSN

—

e-ISSN

—

Počet stran výsledku

5

Strana od-do

95-99

Název nakladatele

IEEE Industrial Electronic Society

Místo vydání

Vienna

Místo konání akce

Timisoara

Datum konání akce

4. 9. 2019

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—