@inproceedings{Brummayer:2008:BBM:1512464.1512472,

title = {BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking},

author = {Robert Brummayer and Armin Biere and Florian Lonsing},

url = {http://doi.acm.org/10.1145/1512464.1512472

https://wp.florianlonsing.com/wp-content/uploads/2024/01/BrummayerBiereLonsing-BPR08.pdf},

doi = {10.1145/1512464.1512472},

isbn = {978-1-60558-440-9},

year  = {2008},

date = {2008-01-01},

urldate = {2008-01-01},

booktitle = {Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning},

pages = {33–38},

publisher = {ACM},

address = {Princeton, New Jersey, USA},

series = {SMT'08/BPR'08},

abstract = {This is a proposal for a bit-precise word-level format, called BTOR. It is easy to parse and has precise semantics. In its basic form it allows to model SMT problems over the quantifier-free 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.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}