SMT-based model checking of data flow programs

Cesare Tinelli

(University of Iowa)

Data flow languages are high level programming languages commonly used in industry to model and implement reactive embedded systems controlling a vast variety of devices.

We present a general approach for proving automatically safety properties of data flow programs. The approach extends and combines Model Checking with Satisfiability Modulo Theories (SMT) techniques. In it, a given program and property are first translated into formulas belonging to a decidable fragment of first-order logic that includes the combined theory of the programs data types -- such as integers, reals, Booleans and so on. Then the property is proved by induction over the length of program executions using as reasoning engine an SMT solver specialized on that theory.

Distinguishing features of this approach are that it scales better than approaches based on propositional reasoning, and it can check safety properties of infinite-state data flow programs as well as finite-state ones. This talk will provide a high level description of the basic approach and its main enhancements as applied to the data flow language Lustre, together with comparative experimental results providing evidence of its effectiveness.
Thursday 22nd July 2010, 14:00
Robert Recorde Room
Department of Computer Science