Many systems can be naturally represented in some decidable fragments of first order logic. The expressive power provided by a background theory allows to describe important aspects such as real time, continuous dynamics, and data flow over integer variables. The corresponding verification problems can be tackled by means of Satisfiability Modulo Theory (SMT) solvers. SMT solvers are based on the tight integration of prepositional SAT solvers with dedicated procedures to reason about the theory component. In this paper, we overview the techniques underlying SMT, we show how to represent dynamic systems in fragments of first order logic, and discuss the application of SMT solvers to their verification.
展开▼
