MathSAT 5

If you would like to cite MathSAT5, please use this reference.

• A. Cimatti, A. Griggio, S. Mover, and S. Tonetta. IC3 Modulo Theories via Implicit Predicate Abstraction. To Appear in proc. TACAS 2014.
• M. Brain, V. D'Silva, A. Griggio, L. Haller, and D. Kroening. Deciding Floating-Point Logic with Abstract Conflict-Driven Clause Learning. Formal Methods in System Design, 2013.
• A. Cimatti, A. Griggio, S. Mover, and S. Tonetta. Parameter Synthesis with IC3. In proc. FMCAD 2013.
• A. Cimatti, A. Griggio, B. Schaafsma, and R. Sebastiani. A Modular Approach to MaxSAT Modulo Theories. In proc. SAT 2013.
• M. Brain, V. D'Silva, A. Griggio, L. Haller, and D. Kroening. Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL. In proc. SAS 2013.
• A. Cimatti, A. Griggio, B. Schaafsma, and R. Sebastiani. The MathSAT5 SMT Solver. In proc. TACAS 2013, Volume 7795 of LNCS, Springer.
• L. Haller, A. Griggio, M. Brain, and D. Kroening. Deciding Floating-Point Logic with Systematic Abstraction. In proc. FMCAD 2012.
• A. Griggio, T. T. H. Le, and Roberto Sebastiani. Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic. Logical Methods in Computer Science, Volume 8, Issue 3, 2012.
• R. Sebastiani and S. Tomasi Optimization in SMT with LA(Q) Cost Functions. In proc. IJCAR 2012.
• A. Cimatti and A. Griggio, Software Model Checking via IC3. In proc. CAV 2012.
• A. Griggio, A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic. JSAT Volume 8(2012), pages 1-27, 2012.
• A. Griggio, Effective Word-Level Interpolation for Software Verification. In proc. FMCAD 2011.
• A. Cimatti, S. Mover, and S. Tonetta. Proving and Explaining the Unfeasibility of Message Sequence Charts for Hybrid Systems. In proc. FMCAD 2011.
• A. Griggio, Q.-S. Phan, R. Sebastiani, and S. Tomasi. Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT. In proc. FroCos 2011.
• A. Cimatti, A. Griggio, A. Micheli, I. Narasamdya, and M. Roveri Kratos -- A Software Model Checker for SystemC. In proc. CAV 2011.
• A. Cimatti, S. Mover, and S. Tonetta. Efficient Scenario Verification for Hybrid Automata. In proc. CAV 2011.
• A. Griggio, T.T.H. Le, and R. Sebastiani. Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic. In proc. TACAS 2011.
• L. Bu, A. Cimatti, X. Li, S. Mover, and S. Tonetta. Model Checking of Hybrid Systems Using Shallow Synchronization. In proc. FORTE 2011.
• A. Griggio, A Practical Approach to SMT(LA(Z)), At SMT'10 Workshop, July 2010.

• Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani. Efficient Interpolant Generation in Satisfiability Modulo Theories. ACM Transations on Computational Logic, TOCL, vol. 12, number 1, October 2010.
• Anders Franzen, Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani, Jonathan Shalev. Applying SMT in Symbolic Execution of Microcode. In proc. FMCAD, 2010.
• Anders Franzen. Efficient Solving of the Satisfiability Modulo Bit-Vectors Problem and Some Extensions to SMT. PhD Thesis, University of Trento, March 2010.
• Alberto Griggio. An Effective SMT Engine for Formal Verification. PhD Thesis, University of Trento, December 2009.
• Alessandro Cimatti, Anders Franzen, Alberto Griggio, Krishnamani Kalyanasundaram, Marco Roveri. Tighter integration of BDDs and SMT for Predicate Abstraction. In proc. DATE, 2010.
• Alessandro Cimatti, Anders Franzen, Alberto Griggio, Roberto Sebastiani, Cristian Stenico. Satisfiability Modulo the Theory of Costs: Foundations and Applications. In proc. TACAS, 2010.
• A. Cimatti, A. Franzen, A. Griggio, K. Kalyanasundaram, M. Roveri. Tighter Integration of BDD and SMT for Predicate Abstraction. In proc. DATE, 2010.
• Dirk Beyer, Alessandro Cimatti, Alberto Griggio, Erkan Keremoglu, Roberto Sebastiani. Software Model Checking via Large-Block Encoding. In Proc. FMCAD, 2009.
• Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani. Interpolant Generation for UTVPI. In Proc. CADE, 2009. LNAI, volume 5663, © Springer.
• Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani. The MathSAT 4 SMT Solver. In Proc. CAV, 2008. LNCS, volume 5123, © Springer.
• Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani. Efficient Interpolant Generation in Satisfiability Modulo Theories. In Proc. TACAS, 2008. LNCS, volume 4963, © Springer.
• Roberto Sebastiani. Lazy Satisfiability Modulo Theories.Journal on Satisfiability, Boolean Modeling and Computation, JSAT. Vol. 3, 2007. Pag 141--224, © IOS Press.
• Roberto Cavada, Alessandro Cimatti, Anders Franzén, K. Kalyanasundaram, Marco Roveri, R.K. Shyamasundar. Computing Predicate Abstractions by Integrating BDDs and SMT Solvers. In Proc. FMCAD, 2007.
• Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti. Verifying Heap-Manipulating Programs in an SMT Framework. In proc. ATVA, 2007. LNCS, volume 4762, © Springer.
• Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Zyiad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani. A Lazy and Layered SMT(BV) Solver for Hard Industrial Verification Problems. In proc. International Conference on Computer-Aided Verification, CAV 2007. July 2007, Berlin. LNCS, volume 4590, © Springer.
• Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani. A Simple and Flexible Way of Computing Small Unsatifiable Cores in Satisfiability Modulo Theories. In proc. Tenth International Conference on Theory and Applications of Satisfiability Testing, SAT 2007. May 28 - 31 2007, Lisbon, Portugal. LNCS, volume 4501, © Springer.
• Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen, Alberto Griggio, Roberto Sebastiani. Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis. In proc. 13th Int. Conference on Logics in Programming, Artificial Intelligence and Reasoning (LPAR'06). Phnom Pehn, Cambodia, 2006 LNAI, volume 4246. © Springer.
• Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani. To Ackermann-ize or not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF U T ). In proc. 13th Int. Conference on Logics in Programming, Artificial Intelligence and Reasoning (LPAR'06). Phnom Pehn, Cambodia, 2006 LNAI, volume 4246. © Springer.
• Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Peter van Rossum, Silvio Ranise, Roberto Sebastiani. Efficient Theory Combination via Boolean Search. Information and Computation. 204(10), 2006. © Elsevier.
• Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Zyiad Hanna, Amit Palti, Zurab Kashidashvili, Roberto Sebastiani. Encoding RTL Constructs for MathSAT: a Preliminary Report. Electronic Notes on Theoretical Computer Science, Volume 144, issue 2, 2006. Ed. Elsevier.
• Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani. MathSAT: A Tight Integration of SAT and Mathematical Decision Procedure. Journal of Automated Reasoning. © Kluwer. Volume 35, Numbers 1-3 / October, 2005.
• Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani. The MathSAT 3 System. In proc. CADE-20, 2005.
• Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Peter van Rossum, Silvio Ranise, Roberto Sebastiani. Efficient Satisfiability Modulo Theories via Delayed Theory Combination. In proc. Int. Conf. on Computer-Aided Verification, CAV 2005. LNCS, No 3576. © Springer.
• Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani. An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. In proc. TACAS'05, Tools and Algorithms for the Construction and Analysis of Systems. Edinburgh, Scotland, April 2005. LNCS, No 3440. © Springer.
• Gilles Audemard, Marco Bozzano, Roberto Sebastiani, Alessandro Cimatti. Verifying Industrial Hybrid Systems with MathSAT. Electronic Notes on Theoretical Computer Science, Volume 119, issue 4, 2004. Ed. Elsevier.
• Gilles Audemard, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani. Bounded Model Checking for Timed Systems. In Proc. 22nd Joint International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2002). Houston, TX, USA, November 2002. . LNCS © Springer.
• Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani. A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. In Proc. 18th "Int. Conference of Automated Deduction, CADE'02." LNAI N.2392 © Springer.