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.

Robert Recorde Room

Department of Computer Science