Leonardo De Moura
Skip Abstract Section
Abstract
Checking the satisfiability of logical formulas, SMT solvers scale orders of magnitude beyond custom ad hoc solvers.
- Audemard, G., Bertoli, P., Cimatti, A., Kornilowicz, A., and Sebastiani, R. A SAT -based approach for solving formulas over Boolean and linear mathematical propositions. In Proceedings of the Conference on Automated Deduction, Vol. 2392 of LNCS (Copenhagen, July 27--30). Springer-Verlag, Berlin, 2002. Google Scholar
Digital Library
- Ball, T. and Rajamani, S.K. The SLAM project: Debugging system software via static analysis. (Symposium on Principles of Programming Languages). SIGPLAN Notices 37, 1 (Jan. 16--18, 2002), 1--3. Google ScholarDigital Library
- Barnett, M., Leino, K.R.M., and Schulte, W. The Spec# programming system: An overview. In Proceedings of the International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices, LNCS 3362 (Marseille, Mar. 10--13). Springer-Verlag, Berlin, 2005, 49--69. Google ScholarDigital Library
- Barrett, C., de Moura, L., and Stump, A. Design and results of the first Satisfiability Modulo Theories Competition. Journal of Automated Reasoning 35, 4 (Nov. 2005), 372--390. Google ScholarDigital Library
- Barrett, C., Dill, D., and Stump, A. Checking satisfiability of first-order formulas by incremental translation to SAT. In Proceedings of the International Conference on Computer Aided Verification (Copenhagen, July, 27--31). Springer-Verlag, Berlin 2002, 236--249. Google ScholarDigital Library
- Barrett, C., Sebastiani, R., Seshia, S.A., and Tinelli, C. Satisfiability Modulo Theories, Vol. 185 of Frontiers in Artificial Intelligence and Applications, Chapter 26. IOS Press, Feb. 2009, 825--885.Google Scholar
- Barrett, C. and Tinelli, C. CVC3. In Proceedings of the 19th International Conference on Computer Aided Verification, Vol. 4590 of LNCS, W. Damm and H. Hermanns, Eds. (Berlin, July 3--7). Springer-Verlag, Berlin, 2007, 298--302. Google ScholarDigital Library
- Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodríguez Carbonell, E., and Rubio, A. The Barcelogic SMT Solver. In Proceedings of the 20th International Conference on Computer Aided Verification, Vol. 5123 of LNCS, A. Gupta and S. Malik, Eds. (Princeton, July 7--14). Springer-Verlag, Berlin, 2008, 294--298. Google ScholarDigital Library
- Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T.A., Ranise, S., van Rossum, P., and Sebastiani, R. Efficient satisfiability modulo theories via delayed theory combination. In Proceedings of the International Conference on Computer Aided Verification, Vol. 3576 of LNCS, K. Etessami and S. K. Rajamani, Eds. (Edinburgh, July 6--12). Springer-Verlag, Berlin, 2005, 335--349. Google ScholarDigital Library
- Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., and Sebastiani, R. The MathSAT 4 SMT Solver. In Proceedings of the 18th International Conference on Computer Aided Verification, Vol. 5123 of LNCS. Springer-Verlag, Berlin, 2008. Google ScholarDigital Library
- Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., and Tobies, S. VCC: A practical system for verifying concurrent C. In Proceedings of the International Conference on Theorem Proving in Higher Order Logics (Munich, Aug. 17--20). Springer-Verlag. Berlin, 2009, 23--42. Google ScholarDigital Library
- Cook, S.A. The complexity of theorem-proving procedures. In Proceedings of the Third Annual ACM Symposium on Theory of Computing (May 3--5). ACM Press, New York, 1971, 151--158. Google ScholarDigital Library
- Davis, M., Logemann, G., and Loveland, D. A machine program for theorem proving. Commun. ACM 5, 2 (July 1962), 394--397. Google ScholarDigital Library
- de Moura, L. and Bjørner, N. Z3: An efficient SMT solver. In Proceedings of the International Conference on tools and algorithms for the Construction and Analysis of Systems, Vol. 4963 of LNCS, C.R. Ramakrishnan and J. Rehof, Eds. (Budapest, Mar. 29- Apr. 6). Springer-Verlag, Berlin, 2008, 337--340. Google ScholarDigital Library
- de Moura, L. and Rueß, H. Lemmas on demand for satisfiability solvers. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (Cincinnati, May 6--9, 2002).Google Scholar
- Detlefs, D., Nelson, G., and Saxe, J.B. Simplify: A theorem prover for program checking. Journal of the ACM 52, 3 (May 2005), 365--473. Google ScholarDigital Library
- Downey, P.J., Sethi, R., and Tarjan, R.E. Variations on the common subexpression problem. Journal of the ACM 27, 4 (Oct. 1980), 758--771. Google ScholarDigital Library
- Dutertre, B. and de Moura, L. A fast linear-arithmetic solver for DPLL(T). In Proceedings of the 16th International Conference on Computer Aided Verification, Vol. 4144 of LNCS (Seattle, Aug. 17--20). Springer-Verlag, Berlin, 2006, 81--94. Google ScholarDigital Library
- Filliâtre, J.-C. Why: A Multi-Language Multi-Prover Verification Tool. Technical Report 1366, Université Paris Sud, 2003.Google Scholar
- Flanagan, C., Joshi, R., Ou, X., and Saxe, J.B. Theorem proving using lazy proof explication. In Proceedings of the 15th International Conference on Computer Aided Verification (Boulder, CO, July 8--12). Springer-Verlag, Berlin, 2003, 355--367.Google ScholarCross Ref
- Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., and Stata, R. Extended static checking for Java. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (Berlin, June 17--19). ACM Press, New York, 2002, 234--245. Google ScholarDigital Library
- Ghilardi, S., Nicolini, E., and Zucchelli, D. A comprehensive framework for combined decision procedures. In Proceedings of the Fifth International Workshop on Frontiers of Combining Systems, Vol. 3717 of LNCS, B. Gramlich, Ed. (Vienna, Sept. 19--21). Springer-Verlag, Berlin, 2005, 1--30. Google ScholarDigital Library
- Godefroid, P., de Halleux, J., Nori, A.V., Rajamani, S.K., Schulte, W., Tillmann, N., and Levin, M.Y. Automating software testing using program analysis. IEEE Software 25, 5 (Sept./Oct. 2008), 30--37. Google ScholarDigital Library
- Grieskamp, W., Kicillof, N., MacDonald, D., Nandan, A., Stobie, K., and Wurden, F.L. Model-based quality assurance of Windows protocol documentation. In Proceedings of the First International Conference on Software Testing, Verification, and Validation (Lillehammer, Norway, Apr. 9--11). IEEE Computer Society Press, 2008, 502--506. Google ScholarDigital Library
- Henzinger, T.A., Jhala, R., Majumdar, R., and Sutre, G. Software verification with blast. In Proceedings of the 10th International SPIN Workshop, Vol. 2648 of LNCS, T. Ball and S. R. Rajamani, Eds. (Portland, May 9--10). Springer-Verlag, Berlin, 2003, 235--239. Google ScholarDigital Library
- Kaufmann, M., Manolios, P., and Moore, J.S. Computer-Aided Reasoning: An Approach. Kluwer Academic, June 2000. Google ScholarDigital Library
- Malik, S. and Zhang, L. Boolean satisfiability from theoretical hardness to practical success. Commun. ACM 52, 8 (Aug. 2009), 76--82. Google ScholarDigital Library
- McCarthy, J. Towards a mathematical science of computation. In Congress of the International Federation for Information Processing, 1962, 21--28.Google Scholar
- Nelson, G. and Oppen, D.C. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1, 2 (Oct. 1979), 245--257. Google ScholarDigital Library
- Nieuwenhuis, R., Oliveras, A., and Tinelli, C. Solving SAT and SAT modulo theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T). Journal of the ACM 53, 6 (Nov. 2006), 937--977. Google ScholarDigital Library
- Oppen, D.C. Complexity, convexity and combinations of theories. Theoretical Computer Science 12, 3 (1980), 291--302.Google ScholarCross Ref
- Owre, S., Rushby, J.M., and Shankar, N. PVS: A prototype verification system. In Proceedings of the 11th International Conference on Automated Deduction (Saratoga, NY, June 15--18). Springer-Verlag, Berlin, 1992, 748--752. Google ScholarDigital Library
- Ranise, S. and Tinelli, C. The Satisfiability Modulo Theories Library (SMT-LIB), 2006; http://www.SMT-LIB.orgGoogle Scholar
- Tinelli, C. and Zarba, C.G. Combining nonstably infinite theories. Journal of Automated Reasoning 34, 3 (Apr. 2005), 209--238. Google ScholarDigital Library
Index Terms
- Satisfiability modulo theories: introduction and applications
Recommendations
Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T)
We first introduce Abstract DPLL, a rule-based formulation of the Davis--Putnam--Logemann--Loveland (DPLL) procedure for propositional satisfiability. This abstract framework allows one to cleanly express practical DPLL algorithms and to formally reason ...
A tutorial on satisfiability modulo theories
CAV'07: Proceedings of the 19th international conference on Computer aided verificationSolvers for satisfiability modulo theories (SMT) check the satisfiability of first-order formulas containing operations from various theories such as the Booleans, bit-vectors, arithmetic, arrays, and recursive datatypes. SMT solvers are extensions of ...
A progressive simplifier for satisfiability modulo theories
SAT'06: Proceedings of the 9th international conference on Theory and Applications of Satisfiability TestingIn this paper we present a new progressive cooperating simplifier for deciding the satisfiability of a quantifier-free formula in the first-order theory of integers involving combinations of sublogics, referred to as Satisfiability Modulo Theories (SMT)...
Comments