Introduction
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
Venue
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].
Proceedings
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).
Deadlines
* 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
Program
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]
[slides]
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” [abstract]
17:45 - 18:00 Closing Remarks and Award Ceremony
