skip to main content
research-article

Abstract conflict driven learning

Published: 23 January 2013 Publication History

Abstract

Modern satisfiability solvers implement an algorithm, called Conflict Driven Clause Learning, which combines search for a model with analysis of conflicts. We show that this algorithm can be generalised to solve the lattice-theoretic problem of determining if an additive transformer on a Boolean lattice is always bottom. Our generalised procedure combines overapproximations of greatest fixed points with underapproximation of least fixed points to obtain more precise results than computing fixed points in isolation. We generalise implication graphs used in satisfiability solvers to derive underapproximate transformers from overapproximate ones. Our generalisation provides a new method for static analysers that operate over non-distributive lattices to reason about properties that require disjunction.

Supplementary Material

JPG File (r2d1_talk5.jpg)
MP4 File (r2d1_talk5.mp4)

References

[1]
B. Badban, J. van de Pol, O. Tveretina, and H. Zantema. Generalizing DPLL and satisfiability for equalities. Information and Computation, 205(8):1188--1211, 2007.
[2]
C. Barrett, R. Nieuwenhuis, A. Oliveras, and C. Tinelli. Splitting on demand in SAT modulo theories. In Proc. of Logic for Programming, Artificial Intelligence, and Reasoning, pages 512--526, 2006.
[3]
M. Brain, V. D'Silva, L. Haller, A. Griggio, and D. Kroening. An abstract interpretation of DPLL(T). In Proc. of Verification, Model Checking and Abstract Interpretation, 2013. To appear.
[4]
E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. J. of the ACM, 50:752--794, 2003.
[5]
S. Cotton. Natural domain SMT: A preliminary assessment. In Proc. of Formal Modeling and Analysis of Timed Systems, pages 77--91, 2010.
[6]
P. Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoretical Computer Science, 277(1-2):47--103, Apr. 2002.
[7]
P. Cousot. Abstract interpretation. MIT course 16.399, Feb.--May 2005.
[8]
P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proc. of Principles of Programming Languages, pages 269--282, 1979.
[9]
P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13:103--179, 1992.
[10]
P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511--547, Aug. 1992.
[11]
P. Cousot and R. Cousot. Refining model checking by abstract interpretation. Automated Software Engineering, 6(1):69--95, 1999.
[12]
P. Cousot, R. Cousot, and L. Mauborgne. The reduced product of abstract domains and the combination of decision procedures. In Proc. of Foundations of Software Science and Computational Structures, pages 456--472, 2011.
[13]
V. D'Silva, L. Haller, and D. Kroening. Satisfiability solvers are static analysers. In Proc. of Static Analysis Symposium, pages 317--333, 2012.
[14]
V. D'Silva, L. Haller, D. Kroening, and M. Tautschnig. Numeric bounds analysis with conflict-driven learning. In Proc. of Tools and Algorithms for the Construction and Analysis of Systems, pages 48--63, 2012.
[15]
H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli. DPLL(T): Fast decision procedures. In Proc. of Computer Aided Verification, pages 175--188, 2004.
[16]
R. Giacobazzi and E. Quintarelli. Incompleteness, counterexamples, and refinements in abstract model-checking. In Proc. of Static Analysis Symposium, pages 356--373, 2001.
[17]
L. Haller, A. Griggio, M. Brain, and D. Kroening. Deciding floatingpoint logic with systematic abstraction. In Proc. of Formal Methods in Computer-Aided Design, pages 131--140, 2012.
[18]
W. R. Harris, S. Sankaranarayanan, F. Ivancic, and A. Gupta. Program analysis via satisfiability modulo path programs. In Proc. of Principles of Programming Languages, pages 71--82, 2010.
[19]
T. A. Henzinger, O. Kupferman, and S. Qadeer. From pre-historic to post-modern symbolic model checking. Formal Methods in Systems Design, 23(3):303--327, Nov. 2003.
[20]
D. Jovanovic and L. M. de Moura. Cutting to the chase - solving linear integer arithmetic. In Proc. of Automated Deduction, pages 338--353, 2011.
[21]
S. Malik and L. Zhang. Boolean satisfiability: From theoretical hardness to practical success. Communications of the ACM, 52:76--82, Aug. 2009.
[22]
K. L. McMillan. Lazy annotation for program testing and verification. In Proc. of Computer Aided Verification, pages 104--118, 2010.
[23]
K. L. McMillan, A. Kuehlmann, and M. Sagiv. Generalizing DPLL to richer logics. In Proc. of Computer Aided Verification, pages 462--476, 2009.
[24]
R. Nieuwenhuis, A. Oliveras, and C. Tinelli. Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). JACM, 53:937--977, 2006.
[25]
X. Rival and L. Mauborgne. The trace partitioning abstract domain. ACM Transactions on Programming Languages and Systems, 29, 2007.
[26]
N. Sörensson and A. Biere. Minimizing learned clauses. In Proc. of Theory and Applications of Satisfiability Testing, pages 237--243, 2009.
[27]
A. Thakur and T. Reps. A Generalization of Stälmarck's Method. In Proc. of Static Analysis Symposium, pages 334--351, 2012.
[28]
A. Thakur and T. Reps. A method for symbolic computation of abstract operations. In Proc. of Computer Aided Verification. Springer, 2012.

Cited By

View all

Index Terms

  1. Abstract conflict driven learning

      Recommendations

      Comments

      Information & Contributors

      Information

      Published In

      cover image ACM SIGPLAN Notices
      ACM SIGPLAN Notices  Volume 48, Issue 1
      POPL '13
      January 2013
      561 pages
      ISSN:0362-1340
      EISSN:1558-1160
      DOI:10.1145/2480359
      Issue’s Table of Contents
      • cover image ACM Conferences
        POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
        January 2013
        586 pages
        ISBN:9781450318327
        DOI:10.1145/2429069
      Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

      Publisher

      Association for Computing Machinery

      New York, NY, United States

      Publication History

      Published: 23 January 2013
      Published in SIGPLAN Volume 48, Issue 1

      Check for updates

      Author Tags

      1. conflict driven clause learning
      2. lattices
      3. satisfiability

      Qualifiers

      • Research-article

      Contributors

      Other Metrics

      Bibliometrics & Citations

      Bibliometrics

      Article Metrics

      • Downloads (Last 12 months)9
      • Downloads (Last 6 weeks)1
      Reflects downloads up to 19 Feb 2025

      Other Metrics

      Citations

      Cited By

      View all
      • (2023)Static Analysis for Data ScientistsChallenges of Software Verification10.1007/978-981-19-9601-6_5(77-91)Online publication date: 22-Jul-2023
      • (2018)Understanding and Extending Incremental Determinization for 2QBFComputer Aided Verification10.1007/978-3-319-96142-2_17(256-274)Online publication date: 18-Jul-2018
      • (2018)Exploring Approximations for Floating-Point Arithmetic Using UppSATAutomated Reasoning10.1007/978-3-319-94205-6_17(246-262)Online publication date: 30-Jun-2018
      • (2017)Using Gate Recognition and Random Simulation for Under-Approximation and Optimized Branching in SAT Solvers2017 IEEE 29th International Conference on Tools with Artificial Intelligence (ICTAI)10.1109/ICTAI.2017.00158(1029-1036)Online publication date: Nov-2017
      • (2016)Automatic Generation of Propagation Complete SAT EncodingsProceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 958310.1007/978-3-662-49122-5_26(536-556)Online publication date: 17-Jan-2016
      • (2015)Conflict-Driven Conditional TerminationComputer Aided Verification10.1007/978-3-319-21668-3_16(271-286)Online publication date: 14-Jul-2015
      • (2015)Abstract Interpretation as Automated DeductionAutomated Deduction - CADE-2510.1007/978-3-319-21401-6_31(450-464)Online publication date: 25-Jul-2015
      • (2014)Model and Proof Generation for Heap-Manipulating ProgramsProceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 841010.1007/978-3-642-54833-8_23(432-452)Online publication date: 5-Apr-2014
      • (2014)Are We There Yet? 20 Years of Industrial Theorem Proving with SPARKInteractive Theorem Proving10.1007/978-3-319-08970-6_2(17-26)Online publication date: 2014
      • (2013)Interpolation-Based Verification of Floating-Point Programs with Abstract CDCLStatic Analysis10.1007/978-3-642-38856-9_22(412-432)Online publication date: 2013
      • Show More Cited By

      View Options

      Login options

      View options

      PDF

      View or Download as a PDF file.

      PDF

      eReader

      View online with eReader.

      eReader

      Figures

      Tables

      Media

      Share

      Share

      Share this Publication link

      Share on social media