On Structural Information and the Experimental Evaluation of SMT Tools

Najet Boughanmi (1) , Silvio Ranise (2) , Christophe Ringeissen (2)

1 TRIO - Real time and interoperability
2 CASSIS - Combination of approaches to the security of infinite states systems

We are interested in studying the impact of various pre-processing transformations of ground formulae on the performances of Satisfiability Modulo Theory tools (based on the integration between an enumerator of truth assignments and a satisfiability procedure for conjunction of literals in some theory) which are supposed to discharge them. We briefly discuss our preliminary experiences.

Domaines: Informatique mobile

Najet Boughanmi, Silvio Ranise, Christophe Ringeissen. On Structural Information and the Experimental Evaluation of SMT Tools. International Workshop on First-Order Theorem Proving - FTP'2005, Sep 2005, Koblenz, Germany. ⟨inria-00105894⟩