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 propositional 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.

Beyond Boolean SAT: Satisfiability Modulo Theories

Cimatti, Alessandro
2008

Abstract

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 propositional 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.
9781424425921
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11582/4550
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact