BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking

Description

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.

Period	14 Jul 2008
Event title	unbekannt/unknown
Event type	Conference
Location	United StatesShow on map