News about Reasoning with Bit-Vectors

Talk by Prof. Armin Biere

Location: APB E005
Start: 1. December 2014 at 10:00 am
End: 1. December 2014 at 11:00 am
Research group: Knowledge Representation and Reasoning
iCal

Bit-Precise reasoning (BPR) in bit-vector logic allows to capture

semantics of systems down to individual bits and thus is essential to many verification and synthesis tasks for both hardware and software systems. As an instance of Satisfiability Modulo Theories (SMT), BPR is in essence about word-level decision procedures for the theory of bit-vectors. In practice, quantifiers and other theory extensions, such as reasoning about arrays, are important too. After a motivating example we give a brief overview on basic techniques for bit-precise reasoning and then will cover more recent theoretical results, including complexity classification results. We discuss challenges in developing an efficient SMT solver for bit-vectors, like our award winning SMT solver Boolector, and in particular present examples, for

which current techniques fail.