Cited By
View all- de Moura LBjørner N(2008)Model-based Theory CombinationElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2008.04.079198:2(37-49)Online publication date: 1-May-2008
SMT(CLU): a step toward scalability in system verification
Pages 844 - 851
Abstract
We describe a SAT-based decision method for the underlying logic in many formal verification problems; i.e. the counter arithmetic logic with lambda expressions and uninterpreted functions (CLU). This logic is well suited for equivalence checking of two versions of a hardware design or the input and output of a compiler and has been recently utilized in several model checkers. Our method follows the general Satisfiability Modulo Theories or SMT(T) framework and combines a DPLL-style SAT solver with two theory solvers; one specific to equality and the other to separation inequality atoms within CLU. By adopting a combined implication scheme, we coordinate the efforts among theory solvers, and by efficiently processing uninterpreted functions involved in conflicts, we considerably improve the effectiveness of SAT learning and backtracking routines. Finally, we empirically demonstrate the effectiveness of our SMT(CLU) procedure and compare its performance to recent solvers on a wide range of hardware verification benchmarks.
References
[1]
E. M. Clarke and E. A. Emerson, "Design and synthesis of synchronization skeletons using branching-time temporal logic," in Logic of Programs, Workshop. London, UK: Springer-Verlag, 1982, pp. 52--71.
[2]
E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, "Counterexample-guided abstraction refinement," in Conference on Computer Aided Verification, 2000, pp. 154--169.
[3]
E. M. Clarke, O. Grumberg, M. Talupur, and D. Wang, "Making predicate abstraction efficient: How to eliminate redundant predicates." in Conference on Computer Aided Verification, 2003, pp. 126--140.
[4]
Z. S. Andraus, M. H. Liffiton, and K. A. Sakallah, "Refinement strategies for verification methods based on datapath abstraction," in ASP-DAC '06: Asia South Pacific design automation, 2006, pp. 19--24.
[5]
R. E. Bryant, S. K. Lahiri, and S. A. Seshia, "Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions," in Proceedings of the 14th International Conference on Computer Aided Verification, 2002, pp. 78--92.
[6]
S. K. Lahiri, S. A. Seshia, and R. E. Bryant, "Modeling and verification of out-of-order microprocessors in UCLID," in FMCAD, 2002, pp. 142--159.
[7]
V. Ganapathy, S. A. Seshia, S. Jha, T. W. Reps, and R. E. Bryant, "Automatic discovery of API-level exploits," in ICSE, May 2005, pp. 312--321.
[8]
C. Tinelli, "A DPLL-based calculus for ground satisfiability modulo theories," in Proceedings of the 8th European Conference on Logics in Artificial Intelligence, 2002, pp. 308--319.
[9]
R. E. Bryant, S. K. Lahiri, and S. A. Seshia, "Deciding CLU logic formulas via Boolean and pseudo-Boolean encodings," in Proc. Intl. Workshop on Constraints in Formal Verification, 2002.
[10]
M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, P. van Rossum, S. Schulz, and R. Sebastiani, "An incremental and layered procedure for the satisfiability of linear arithmetic logic." in TACAS, 2005, pp. 317--333.
[11]
H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli, "DPLL(T): Fast decision procedures," in CAV, 2004, pp. 175--188.
[12]
H. M. Sheini and K. A. Sakallah, "A SAT-based decision procedure for mixed logical/integer linear problems." in CPAIOR, 2005, pp. 320--335.
[13]
R. Nieuwenhuis and A. Oliveras, "DPLL(T) with exhaustive theory propagation and its application to difference logic." in Conference on Computer Aided Verification, 2005, pp. 321--334.
[14]
N. Eén and N. Sörensson, "An extensible SAT-solver." in SAT, 2003, pp. 502--518.
[15]
S. A. Seshia, S. K. Lahiri, and R. E. Bryant, "A hybrid SAT-based decision procedure for separation logic with uninterpreted functions," in DAC. New York, NY, USA: ACM Press, 2003, pp. 425--430.
[16]
W. Ackermann, "Solvable cases of the decision problem," in Studies in Logic and the Foundations of Mathematics. North-Holland, 1954.
[17]
R. Nieuwenhuis and A. Oliveras, "Decision procedures for SAT, SAT modulo theories and beyond, the BarcelogicTools." in Conf. Logic for Programming, Artificial Intelligecne and Reasoning, 2005, pp. 23--46.
[18]
R. Nieuwenhuis and A. Oliveras, "Proof-Producing Congruence Closure," in Proceedings of the 16th Int'l Conf. on Term Rewriting and Applications, 2005, pp. 453--468.
[19]
C. W. Barrett and S. Berezin, "CVCLite: A new implementation of the cooperating validity checker category b." in CAV, 2004, pp. 515--518.
[20]
P. Marques-Silva and K. A. Sakallah, "GRASP: A search algorithm for propositional satisfiability," IEEE Trans. Comput., vol. 48, no. 5, pp. 506--521, 1999.
[21]
J. Jaffar, M. J. Maher, P. J. Stuckey, and R. H. C. Yap, "Beyond finite domains," in Workshop on Principles and Practice of Constraint Programming, 1994, pp. 86--94.
[22]
P. Manolios and S. K. Srinivasan, "A parameterized benchmark suite of hard pipelined-machine-verification problems." in CHARME, 2005, pp. 363--366.
[23]
L. de Moura, "Yices," 2005. {Online}. Available: http://fm.csl.sri.com/yices/
Index Terms
- SMT(CLU): a step toward scalability in system verification
Recommendations
SAT and SMT: Their Algorithm Designs and Applications
APSEC '13: Proceedings of the 2013 20th Asia-Pacific Software Engineering Conference (APSEC) - Volume 02SAT and SMT (SAT modulo theory) solvers aim to find a satisfiable instance of given constraints. SAT solver accepts a boolean constraints in a conjunctive normal form (CNF), such as, and if a CNF is satisfiable, returns an instance, such as. SMT solver ...
Approximating Quantified SMT-Solving with SAT
SSIRI-C '11: Proceedings of the 2011 Fifth International Conference on Secure Software Integration and Reliability Improvement - CompanionSatisfiability Modulo Theories (SMT) is an extension of SAT towards FOL. SMT solvers have proven highly scalable and efficient for problems based on some ground theorems. However, SMT problems involving quantifiers and combination of theorems is a long-...
Learning SMT(LRA) constraints using SMT solvers
IJCAI'18: Proceedings of the 27th International Joint Conference on Artificial IntelligenceWe introduce the problem of learning SMT(LRA) constraints from data. SMT(LRA) extends propositional logic with (in)equalities between numerical variables. Many relevant formal verification problems can be cast as SMT(LRA) instances and SMT(LRA) has ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2006 ACM.
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]
Sponsors
- SIGDA: ACM Special Interest Group on Design Automation
- IEEE-CAS: Circuits & Systems
- IEEE-CS: Computer Society
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 05 November 2006
Check for updates
Qualifiers
- Article
Conference
ICCAD06
Sponsor:
- SIGDA
- IEEE-CAS
- IEEE-CS
ICCAD06: The International Conference on Computer-Aided Design 2006
November 5 - 9, 2006
California, San Jose
Acceptance Rates
Overall Acceptance Rate 457 of 1,762 submissions, 26%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 130Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 13 Nov 2024
Other Metrics
Citations
Cited By
View all- de Moura LBjørner N(2008)Model-based Theory CombinationElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2008.04.079198:2(37-49)Online publication date: 1-May-2008
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in