Grande Salle de VERIMAG
4 mars 2010 - 14h00
Code analysis with Blast
par Ondrej Sery de Charles University Prague
Abstract: The first part of the talk will present the Blast model checker, which has originated at UC Berkley (Ranjit Jhala, Rupak Majumdar, Gregoire Sutre) and has been thereafter developed also at other institutions, e.g., EPFL Lausanne (T. Henzinger), UC San Diego (Ranjit Jhala), UC Los Angeles (Rupak Majumdar), Simon Fraser University (Dirk Beyer).
Blast is a counter-example guided abstraction refinement model checker for C programs, which features two important optimization techniques: lazy abstraction and interpolation-based refinement. Lazy abstraction refers to on-the-fly construction of the abstract state space and refinement of only the necessary portions of the abstract state space. This is in contrast to reconstruction of the entire Boolean program in every refinement loop. Moreover, Blast can assign different predicates to different program locations and thus track only the information that is important at the particular location. The mapping of predicates to program locations is a product of interpolation-based refinement, which derives the predicates from the proof of unsatisfiablity of trace formulas corresponding to spurious error traces.
In the second part, I will summarize my contribution regarding the Blast model checker. I have implemented a behavior specification extension that employs a simple regular language (based on behavior protocols). The state space of the property specification is tracked separately from the actual code, i.e., without any code modification. In contrast, properties expressed in the Blast specification language get incorporated into the code itself. This way, the code gets inflated and additional artificial predicates have to be managed by the tool.
In cooperation with ABB Germany, we have employed Blast in an industrial case study. We analyzed the C implementation of the OPC UA communication protocol. On the one hand, the case study revealed real bugs in the implementation that were confirmed by the developers. On the other hand, we identified several shortcomings of the tool itself.
