Abstract: Recent progress in decision procedures has made precise handling of bit-vectors not only practical, but also performance-competitive with classical approaches based on unbounded integers and rationals, while offering sound treatment of boundary conditions and precise reasoning about nonlinear arithmetic.

After a quick introduction to bit-vector arithmetic, this talk presents two novel techniques for improving performance of bit-vector decision procedures, namely structural abstraction and automatic search parameter tuning.

Structural abstraction has been usefully applied to checking of large software verification conditions, where it effectively abstracts away expressions corresponding to irrelevant function calls.

Automatic tuning can improve a state-of-the-art decision procedure for large, real-world bounded model-checking and software verification instances. The resulting, automatically-derived parameter settings yielded runtimes on average 4.5 times faster on bounded model checking instances and 500 times faster on software verification problems than extensive hand-tuning of the decision procedure. Furthermore, the availability of automatic tuning influenced the design of the solver, and the automatically-derived parameter settings provided a deeper insight into the properties of problem instances.

Domagoj Babic is a Ph.D. candidate at the University of British Columbia. His research interests include software verification and analysis, as well as automated theorem proving and SAT solving. Domagoj is currently working on a scalable and precise static checker Calysto, and a bit-vector decision procedure Spear for software verification. He is planning to graduate in early spring 2008. Domagoj holds a M.Sc. degree in computer science and a Dipl.Ing. degree in industrial electronics from the Faculty of Electrical Engineering and Computing at Zagreb University. He is a Microsoft fellow (2005-2007). Appointments: dcm@cs.cmu.edu