Model Checking Using SMT and Theory of Lists

12 years 11 months ago

Download research.microsoft.com

A main idea underlying bounded model checking is to limit the length of the potential counter-examples, and then prove properties for the bounded version of the problem. In software model checking, that means that only program traces up to a given length are considered. Additionally, the program’s input space must be made ﬁnite by deﬁning bounds for all input parameters. To ensure the ﬁniteness of the program traces, these techniques typically require that all loops are explicitly unrolled some constant number of times. Here, we show how to avoid explicit loop unrolling by using the SMT Theory of Lists to model feasible, potentially unbounded program traces. We argue that this approach is easier to use, and, more importantly, increases the conﬁdence in veriﬁcation results over the typical bounded approach. To demonstrate the feasibility of this idea, we implemented a fully automated prototype software model checker and veriﬁed several example algorithms. We also applied o...

Aleksandar Milicevic, Hillel Kugler

Real-time Traffic