Satisfiability Modulo Theories (SMT) can be seen as an extended form of propositional satisfiability, where propositions are either simple boolean propositions or quantifier-free atomic constraints, in a specific theory. In this paper we present MathSAT version 3, a DPLL-based decision procedure for the SMT problem for various theories, including those of Equality and Uninterpreted Functions, of Separation Logic, and of Linear Arithmetic on Reals and on the integers

The Mathsat3 System

Bozzano, Marco;Bruttomesso, Roberto;Cimatti, Alessandro;Sebastiani, Roberto
2005-01-01

Abstract

Satisfiability Modulo Theories (SMT) can be seen as an extended form of propositional satisfiability, where propositions are either simple boolean propositions or quantifier-free atomic constraints, in a specific theory. In this paper we present MathSAT version 3, a DPLL-based decision procedure for the SMT problem for various theories, including those of Equality and Uninterpreted Functions, of Separation Logic, and of Linear Arithmetic on Reals and on the integers
2005
9783540280057
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: https://hdl.handle.net/11582/2407
 Attenzione

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

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