News about Reasoning with Bit-Vectors

Vortrag von Prof. Armin Biere

Veranstaltungsort: APB E005
Beginn: 1. Dezember 2014 um 10:00
Ende: 1. Dezember 2014 um 11:00
Forschungsgruppe: Wissensverarbeitung
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.