Using Satisfiability Modulo Theories for Inductive Verification of Lustre Programs

The problem of verifying safety properties of Lustre programs with integer arithmetic have been attacked in several different ways. Abstract interpretation is used in NBAC, and inductive verification using a SAT solver is used in Luke.This paper presents a method of using Satisfiability Modulo Theories (SMT) as an incremental decision procedure for inductive verification of Lustre program. We show that even a very naive approach using SMT is competitive and in some instances complementary to other approaches.