Bit-Precise Reasoning 2009

Second International Workshop

June 27, Grenoble, France, CAV'09

[ history | overview | scope  ]

News

Unfortunately, due to too much overlap with closely related workshops and lack of original papers we decided to cancel the workshop.

History

The first workshop on Bit-Precise Reasoning (BPR'08) took place in Princeton in 2008 and was also affiliated to CAV.

Overview

Bit-precise reasoning (BPR) is a new and promising trend in automated theorem proving. Traditionally, many theorem provers approximate bit-vector arithmetic by unbounded integers or even floating-point. Such approximations fail to model the boundary behavior of bit-vector arithmetic (overflows and underflows) accurately. In addition, reasoning about non-linear operators over unbounded integers is particularly problematic (undecidable). Recent advances in bit-vector arithmetic decision procedures indicate that BPR could become a practical method capable of handling both boundary conditions and nonlinear operators precisely.

In the last couple of years, many novel techniques have been proposed for reasoning about bit-vectors. Many of those techniques are partially based on boolean satisfiability (SAT) solvers, which have experienced an unprecedented boost in performance of several orders of magnitude over the last decade. This impressive progress creates new opportunities and attracts more and more researchers to BPR. Due to such an abundance of new results, SMT papers are published in several conferences such as CADE, CAV, CP, FMCAD, and SAT, thus making it harder for researchers to get together and discuss their new ideas or implementations. The BPR Workshop attempts to mitigate this problem by providing a forum exclusively dedicated to BPR. Its collocation with CAV is of special interest since this will also allow BPR researchers to interact with the verification community, the area in which BPR has been most successfully applied.

Aims and Scope of the Workshop

The primary goal of the BPR Workshop is to bring together both researchers and users of BPR technology and provide them with a forum for presenting and discussing not only new theoretical ideas, but also implementation and evaluation techniques that, due to either their premature state or their experimental nature, are unlikely to be accepted for publication in larger conferences.

As far as the scope of the workshop is concerned, we want to remark that the ultimate goal in BPR is to develop techniques that have real applications. This is why we believe that collocation with CAV is the ideal situation since, currently, the main advances in BPR research seem to be verification-oriented. However, we understand BPR in a broader sense. The scope of the workshop also includes uses of BPR for more general automated reasoning purposes, relations with other areas such as SAT solving or constraint programming, and even theoretical ideas that may give new insights about how to improve current state-of-the-art tools.