Robert Brummayer, Florian Lonsing, Armin Biere,
"BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking"
: Proc. 1st Intl. Workshop on Bit-Precise Reasoning (BPR'08), 2008
Original Titel:
BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 1st Intl. Workshop on Bit-Precise Reasoning (BPR'08)
Original Kurzfassung:
This is a proposal for a bit-precise word-level format, called
BTOR. It is easy to parse, has precise semantics and in its basic form
allows to model SMT problems over the theory of bit-vectors in combination
with one-dimensional arrays. Our main contribution is a sequential
extension that can be used to capture model checking problems on the
word-level. We present two case studies where BTOR is used as sequential
format. Finally, we report on experimental results for the model
checking extension of our SMT solver Boolector.
Forschungs-