Title of the talk: "Conditional Model Checking"
On October 25, 2011, Professor Dr. Dirk Beyer will give a talk about "Conditional Model Checking" in the context of the SFB 901 colloquium.
Abstract:
Software model checking has received increasing attention in the software-engineering community, due to its high precision in finding bugs. The effectiveness could be further improved by combining techniques and benefit from complementary strengths of different techniques. The usual combination as reduced product, where information can be transferred between analyses that run in parallel, is useful to improve both precision and performance.
We refer to this as parallel combination. However, this method does not work well if the techniques are based on different algorithms, are only available as binaries, or only compilable on incompatible platforms. In this paper, we experimentally investigate the possibilities that rise from sequential combination, which means to run different techniques sequentially one after the other, and information is transferred from one as output, to the next technique as input. To make this possible, we define conditional model checking, which expects as input conditions that instruct the model checker to verify certain parts of the state space, and outputs another condition that summarizes the performed work. This way, the summary condition produced by one model checker can be given as input to another model checker, which in turn performs a conditional analysis only on the remaining state space as specified by the input condition. Our experimental investigation shows that sequential combination of techniques can improve performance as well as effectiveness, i.e., we can now verify programs that we could not before.