2013 28th IEEE/ACM International Conference on Automated Software Engineering (ASE), November 11-15, 2013, Palo Alto, USA

Desktop Layout

Technical Research Track
Medtrn. II
Blitz: Compositional Bounded Model Checking for Real-World Programs
Chia Yuan Cho, Vijay D’Silva, and Dawn Song
(University of California at Berkeley, USA)
Abstract: Bounded Model Checking (BMC) for software is a precise bug-finding technique that builds upon the efficiency of modern SAT and SMT solvers. BMC currently does not scale to large programs because the size of the generated formulae exceeds the capacity of existing solvers. We present a new, compositional and property-sensitive algorithm that enables BMC to automatically find bugs in large programs. A novel feature of our technique is to decompose the behaviour of a program into a sequence of BMC instances and use a combination of satisfying assignments and unsatisfiability proofs to propagate information across instances. A second novelty is to use the control- and data-flow of the program as well as information from proofs to prune the set of variables and procedures considered and hence, generate smaller instances. Our tool BLITZ outperforms existing tools and scales to programs with over 100,000 lines of code. BLITZ automatically and efficiently discovers bugs in widely deployed software including new vulnerabilities in Internet infrastructure software.


Time stamp: 2019-07-23T15:09:25+02:00