Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Model Checking Using SMT and Theory of Lists

Aleks Milicevic and Hillel Kugler

Abstract

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 finite by defining bounds for all input parameters. To ensure the finiteness 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 confidence in verification results over the typical bounded approach. To demonstrate the feasibility of this idea, we implemented a prototype software model-checker and verified several example algorithms. We also applied our technique to a non software model-checking problem from biology – we used it to analyze and synthesize correct executions from scenario-based requirements.

Details

Publication typeInproceedings
Published inNasa Formal Methods Symposium
URLhttp://dx.doi.org/10.1007/978-3-642-20398-5_21
Pages282-297
Volume6617
SeriesLNCS
PublisherSpringer Verlag
> Publications > Model Checking Using SMT and Theory of Lists