Code analysis with Blast

The first part of the talk will present the Blast model checker, which has originated at UC Berkley. 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.

In the second part, I will summarize my own 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.