Domagoj Babic


Bit-Precise Reasoning is increasingly being used for the analysis of many real world hardware and software systems. Current applications include microcode validation, word-level model checking, software verification, equivalence checking and random testcase generation. The continued success in these and other applications depends on the development of more efficient decision procedures for bit-precise reasoning, their combination with decision procedures for other theories (e.g. the theory of arrays), as well as domain-specific techniques to further increase the scalability of the analysis.

The goal of this workshop is to bring together researchers in Bit-Precise Reasoning with industrial users. Topics of interest include, but are not limited to:

* Case studies and applications

* New decision procedures and novel implementation techniques

* Combination with other theories

* Theoretical results

* Benchmarks and evaluation methodologies


Princeton, New Jersey. July 14th, 2008. Affiliated with CAV 2008.

Paper Submission

Original Papers that have not been previously published or submitted (simultaneous submissions are not allowed). Tutorial / survey papers are encouraged. Given the informal style of the workshop, work in progress will be welcome. Papers must be less than 12 pages long, including appendices, and will be published in the proceedings to be distributed to the participants.


Presentation-only Papers describing work recently published or submitted. These papers will not be published in the proceedings.


Both kinds of submissions will be peer reviewed.

Submission format:
LaTeX article format, 11 pt, one column, standard margins, a4paper, max 12 pages.

Submit via EasyChair: [submission link].


Given the informal nature of the workshop, only informal proceedings will be distributed at the workshop. We are planning to publish a selected subset of the submitted papers as post-proceedings in a special volume of the Electronic Notes in Theoretical Computer Science (ENTCS).


* Submission:                May 5th, 2008

* Notification:                 June 2nd, 2008

* Final version:               June 9th, 2008

* Workshop:                   July 14th, 2008

Fortify Best Student BPR Paper Award

A 1000$ US award was given to the best original student paper. The award was sponsored by Fortify Software.


The award went to:

             Robert Brummayer
Florian Lonsing
For the “BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking” paper.


Program Committee

Domagoj Babic (co-chair), University of British Columbia

Amit Goel (co-chair), Intel Corporation

Per Bjesse, Synopsys, Inc.

Alessandro Cimatti, ITC-Irst, Trento

Jim Grundy, Intel Corporation

Ranjit Jhala, University of California, San Diego

Pete Manolios, Northeastern University

Leonardo de Moura, Microsoft Research

Ofer Strichman, Technion - Israel Institute of Technology

Karen Yorav, IBM



 9:00 -  9:15  Opening Remarks
 9:15 - 10:30  Daniel Kroening:
A Bitwise World” [abstract][slides]
10:30 - 11:00  Break I
11:00 - 12:30  Reasoning Session

  11:00 - 11:30  N.Kettle and A.King:
Bit-Precise Reasoning with Affine Functions
11:30 - 12:00  N.He and M.Hsiao: “A New Testability   
  Guided Abstraction to Solving Bit-vector Formula

12:00 - 12:30  P.Kalla, N.Tew, N.Shekhar, and
  S.Gopalakrishnan: “
RTL Verification of Arithmetic 
  Datapaths using Finite Integer Algebras

12:30 - 14:00  Lunch
14:00 - 15:30  John R. Harrison: “Floating-point
               reasoning at the bit level
” [abstract]  
15:30 - 16:00  Break II
16:00 - 17:45  Applications Session

  16:00 - 16:30  E.Smith and D.Dill: “Automatic Formal  
  Verification of Block Cipher Implementations

16:30 - 17:00  R.Brummayer, A.Biere, and F.Lonsing:
BTOR: Bit-Precise Modelling of Word-Level Problems
  for Model Checking

17:00 - 17:45  John Matthews:
  “Challenges in Equivalence Checking Public-Key
  Cryptography Primitives” [

17:45 - 18:00  Closing Remarks and Award Ceremony


BPR 2008

1st International Workshop on Bit-Precise Reasoning

Bit-Precise Reasoning Workshop