More Web Proxy on the site http://driver.im/

research-article

Control flow-guided SMT solving for program verification

Authors:

Fei HeAuthors Info & Claims

ASE '18: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering

Pages 351 - 361

https://doi.org/10.1145/3238147.3238218

Published: 03 September 2018 Publication History

Abstract

Satisfiability modulo theories (SMT) solvers have been widely applied as the reasoning engine for diverse software analysis and verification technologies. The efficiency of the SMT solver has significant effects on the performance of these technologies. However, the current SMT solvers are designed for the general purpose of constraint solving. Many useful knowledge of programs cannot be utilized during the SMT solving. As a result, the SMT solver may spend a lot of effort to explore redundant search space. In this paper, we propose a novel approach for utilizing control-flow knowledge in SMT solving. With this technique, the search space can be considerably reduced and the efficiency of SMT solving is observably improved. We conducted extensive experiments on credible benchmarks, the results show orders of magnitude improvements of our approach.

References

[1]

Mike Barnett, Manuel Fähndrich, K Rustan M Leino, Peter Müller, Wolfram Schulte, and Herman Venter. 2011.

[2]

Specification and verification: the Spec# experience. Commun. ACM 54, 6 (2011), 81–91.

Digital Library

[3]

Jason Belt, Xianghua Deng, et al. 2009. Sireum/Topi LDP: a lightweight semidecision procedure for optimizing symbolic execution-based analyses. In Proceedings of the the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering. ACM, 355–364.

Digital Library

[4]

Murphy Berzish, Yunhui Zheng, and Vijay Ganesh. 2017. Z3str3: A string solver with theory-aware branching. arXiv preprint arXiv:1704.07935 (2017).

[5]

Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M Erkan Keremoglu, and Roberto Sebastiani. 2009. Software model checking via large-block encoding. In Formal Methods in Computer-Aided Design, 2009. FMCAD 2009. IEEE, 25–32.

[6]

Dirk Beyer, Matthias Dangl, and Philipp Wendler. 2018.

[7]

A unifying view on SMT-based software verification. Journal of Automated Reasoning 60, 3 (2018), 299–335.

Digital Library

[8]

Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. 1999. Symbolic model checking without BDDs. In International conference on tools and algorithms for the construction and analysis of systems. Springer, 193–207.

Digital Library

[9]

Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh. 2009. Conflictdriven clause learning SAT solvers. Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications (2009), 131–153.

[10]

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Peter Van Rossum, Stephan Schulz, and Roberto Sebastiani. 2005. The mathsat 3 system. In International Conference on Automated Deduction. Springer, 315–321.

Digital Library

[11]

Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, and Roberto Sebastiani. 2007. A Lazy and Layered SMT ( B V) Solver for Hard Industrial Verification Problems. In International Conference on Computer Aided Verification. Springer, 547–560.

Digital Library

[12]

Alessandro Cimatti, Jori Dubrovin, Tommi Junttila, and Marco Roveri. 2009.

[13]

Structure-aware computation of predicate abstraction. In Formal Methods in Computer-Aided Design, 2009. FMCAD 2009. IEEE, 9–16.

[14]

Edmund Clarke, Daniel Kroening, and Flavio Lerda. 2004. A tool for checking ANSI-C programs. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 168–176.

[15]

Patrick Cousot and Radhia Cousot. 1977.

[16]

Ron Cytron, Jeanne Ferrante, Barry K Rosen, Mark N Wegman, and F Kenneth Zadeck. 1989. An efficient method of computing static single assignment form. In Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, 25–35.

Digital Library

[17]

Martin Davis, George Logemann, and Donald Loveland. 1962. A machine program for theorem-proving. Commun. ACM 5, 7 (1962), 394–397.

Digital Library

[18]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337–340.

Digital Library

[19]

Leonardo De Moura and Nikolaj Bjørner. 2011. Satisfiability modulo theories: introduction and applications. Commun. ACM 54, 9 (2011), 69–77. Control Flow-Guided SMT Solving for Program Verification ASE ’18, September 3–7, 2018, Montpellier, France

Digital Library

[20]

Alastair F Donaldson, Leopold Haller, Daniel Kroening, and Philipp Rümmer. 2011.

[21]

Software verification using k-induction. In International Static Analysis Symposium. Springer, 351–368.

Digital Library

[22]

Herbert Enderton and Herbert B Enderton. 2001.

[23]

A mathematical introduction to logic. Academic press.

[24]

Josselin Feist, Laurent Mounier, and Marie-Laure Potet. 2016. Guided dynamic symbolic execution using subgraph control-flow information. In International Conference on Software Engineering and Formal Methods. Springer, 76–81.

[25]

Jon William Freeman. 1995.

[26]

Improvements to propositional satisfiability search algorithms. Ph.D. Dissertation. University of Pennsylvania Philadelphia, PA.

[27]

Dan Goldwasser, Ofer Strichman, and Shai Fine. 2008.

[28]

A theory-based decision heuristic for DPLL (T). In Formal Methods in Computer-Aided Design, 2008. FMCAD’08. IEEE, 1–8.

Digital Library

[29]

Susanne Graf and Hassen Saïdi. 1997. Construction of abstract state graphs with PVS. In International Conference on Computer Aided Verification. Springer, 72–83.

Digital Library

[30]

Aarti Gupta, Malay Ganai, Chao Wang, Zijiang Yang, and Pranav Ashar. 2003.

[31]

Learning from BDDs in SAT-based bounded model checking. In Proceedings of the 40th annual Design Automation Conference. ACM, 824–829.

Digital Library

[32]

Pieter Hooimeijer and Westley Weimer. 2010. Solving string constraints lazily. In Proceedings of the IEEE/ACM international conference on Automated software engineering. ACM, 377–386.

Digital Library

[33]

Robert G Jeroslow and Jinchang Wang. 1990. Solving propositional satisfiability problems. Annals of mathematics and Artificial Intelligence 1, 1-4 (1990), 167–187.

Digital Library

[34]

James C King. 1976. Symbolic execution and program testing. Commun. ACM 19, 7 (1976), 385–394.

Digital Library

[35]

Daniel Kroening and Michael Tautschnig. 2014. CBMC–C bounded model checker. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 389–391.

[36]

Andreas Kuehlmann, Malay K Ganai, and Viresh Paruthi. 2001. Circuit-based Boolean reasoning. In Proceedings of the 38th annual Design Automation Conference. ACM, 232–237.

Digital Library

[37]

K Rustan M Leino, Michał Moskal, and Wolfram Schulte. 2008.

[38]

Verification condition splitting. Submitted manuscript, September (2008).

[39]

Jia Hui Liang, Vijay Ganesh, Ed Zulkoski, Atulan Zaman, and Krzysztof Czarnecki. 2015. Understanding VSIDS branching heuristics in conflict-driven clauselearning SAT solvers. In Haifa Verification Conference. Springer, 225–241.

[40]

Joao Marques-Silva. 1999. The impact of branching heuristics in propositional satisfiability algorithms. In Portuguese Conference on Artificial Intelligence. Springer, 62–74.

Digital Library

[41]

Matthew W Moskewicz, Conor F Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. 2001. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th annual Design Automation Conference. ACM, 530–535.

Digital Library

[42]

Greg Nelson and Derek C Oppen. 1980.

[43]

Fast decision procedures based on congruence closure. Journal of the ACM (JACM) 27, 2 (1980), 356–364.

Digital Library

[44]

Alexandru Nicolau. 1988.

[45]

Loop quantization: A generalized loop unwinding technique. J. Parallel and Distrib. Comput. 5, 5 (1988), 568–586.

Digital Library

[46]

Richard Ostrowski, Éric Grégoire, Bertrand Mazure, and Lakhdar Sais. 2002.

[47]

Recovering and exploiting structural knowledge from CNF formulas. In International Conference on Principles and Practice of Constraint Programming. Springer, 185–199.

Digital Library

[48]

Marco Pistoia, Satish Chandra, Stephen J Fink, and Eran Yahav. 2007. A survey of static analysis methods for identifying security vulnerabilities in software systems. IBM Systems Journal 46, 2 (2007), 265–288.

Digital Library

[49]

M Prasanna, S Sivanandam, R Venkatesan, and R Sundarrajan. 2005. A survey on automatic test case generation. Academic Open Internet Journal 15, 6 (2005).

[50]

Daniele Pretolani. 1996. Efficiency and stability of hypergraph SAT algorithms. DIMACS Series in Discrete Mathematics and Theoretical Computer Science 26 (1996), 479–498.

[51]

Sriram Sankaranarayanan, Henny B Sipma, and Zohar Manna. 2004. Non-linear loop invariant generation using Gröbner bases. ACM SIGPLAN Notices 39, 1 (2004), 318–329.

Digital Library

[52]

Ofer Shtrichman. 2000. Tuning SAT checkers for bounded model checking. In International Conference on Computer Aided Verification. Springer, 480–494.

Digital Library

[53]

Niklas Sorensson and Niklas Een. 2005. Minisat v1. 13-a sat solver with conflictclause minimization. SAT 2005, 53 (2005), 1–2.

[54]

G Tseitin. 1968. On the complexity of derivation in propositional calculus. Studies in Constrained Mathematics and Mathematical Logic (1968).

[55]

Chao Wang, HoonSang Jin, Gary D Hachtel, and Fabio Somenzi. 2004. Refining the SAT decision ordering for bounded model checking. In Proceedings of the 41st annual Design Automation Conference. ACM, 535–538.

Digital Library

Cited By

Liu ZLuo NJudson SDutta RGuo XSantolucito MLuo BLiao XXu JKirda ELie D(2024)Poster: BlindMarket: A Trustworthy Chip Designs Marketplace for IP Vendors and UsersProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3691378(5048-5050)Online publication date: 2-Dec-2024
https://dl.acm.org/doi/10.1145/3658644.3691378
Fang XDing FHuang BWang ZHan GYang RYou LXiang QKong LLiu YShu J(2024)Network Can Help Check Itself: Accelerating SMT-based Network Configuration Verification Using Network Domain KnowledgeIEEE INFOCOM 2024 - IEEE Conference on Computer Communications10.1109/INFOCOM52122.2024.10621215(2119-2128)Online publication date: 20-May-2024
https://doi.org/10.1109/INFOCOM52122.2024.10621215
Zhang YXie XLi YLin YChen SLiu YLi X(2023)Demystifying Performance Regressions in String SolversIEEE Transactions on Software Engineering10.1109/TSE.2022.316837349:3(947-961)Online publication date: 1-Mar-2023
https://doi.org/10.1109/TSE.2022.3168373
Show More Cited By

Index Terms

Control flow-guided SMT solving for program verification
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
2. Theory of computation
  1. Logic
    1. Logic and verification

Recommendations

Interference relation-guided SMT solving for multi-threaded program verification
PPoPP '22: Proceedings of the 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming

Concurrent program verification is challenging due to a large number of thread interferences. A popular approach is to encode concurrent programs as SMT formulas and then rely on off-the-shelf SMT solvers to accomplish the verification. In most existing ...
Leveraging Control Flow Knowledge in SMT Solving of Program Verification
Continuous Special Section: AI and SE

Satisfiability modulo theories (SMT) solvers have been widely applied as the reasoning engine for diverse software analysis and verification technologies. The efficiency of the SMT solver has significant effects on the performance of these technologies. ...
Fast bit-vector satisfiability
ISSTA 2020: Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis

SMT solving is often a major source of cost in a broad range of techniques such as symbolic program analysis. Thus, speeding up SMT solving is still an urgent requirement. A dominant approach, which is known as eager SMT solving, is to reduce a first-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ASE '18: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering

September 2018

955 pages

ISBN:9781450359375

DOI:10.1145/3238147

General Chair:
Marianne Huchard
University of Montpellier, France
,
Program Chairs:
Christian Kästner
Carnegie Mellon University, USA
,
Gordon Fraser
University of Passau, Germany

Copyright © 2018 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 the author(s) 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

SIGAI: ACM Special Interest Group on Artificial Intelligence
CNRS: Centre National De La Rechercue Scientifique
SIGSOFT: ACM Special Interest Group on Software Engineering
IEEE-CS: Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 September 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Distinguished Paper

Author Tags

Qualifiers

Research-article

Funding Sources

National Natural Science Foundation of China

Conference

ASE '18

Sponsor:

SIGAI
CNRS
SIGSOFT
IEEE-CS

ASE '18: 33rd ACM/IEEE International Conference on Automated Software Engineering

September 3 - 7, 2018

Montpellier, France

Acceptance Rates

Overall Acceptance Rate 82 of 337 submissions, 24%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
636
Total Downloads

Downloads (Last 12 months)94
Downloads (Last 6 weeks)11

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Liu ZLuo NJudson SDutta RGuo XSantolucito MLuo BLiao XXu JKirda ELie D(2024)Poster: BlindMarket: A Trustworthy Chip Designs Marketplace for IP Vendors and UsersProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3691378(5048-5050)Online publication date: 2-Dec-2024
https://dl.acm.org/doi/10.1145/3658644.3691378
Fang XDing FHuang BWang ZHan GYang RYou LXiang QKong LLiu YShu J(2024)Network Can Help Check Itself: Accelerating SMT-based Network Configuration Verification Using Network Domain KnowledgeIEEE INFOCOM 2024 - IEEE Conference on Computer Communications10.1109/INFOCOM52122.2024.10621215(2119-2128)Online publication date: 20-May-2024
https://doi.org/10.1109/INFOCOM52122.2024.10621215
Zhang YXie XLi YLin YChen SLiu YLi X(2023)Demystifying Performance Regressions in String SolversIEEE Transactions on Software Engineering10.1109/TSE.2022.316837349:3(947-961)Online publication date: 1-Mar-2023
https://doi.org/10.1109/TSE.2022.3168373
Wang CFan GYao PPan FZhang C(2023)Verifying Data Constraint Equivalence in FinTech Systems2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)10.1109/ICSE48619.2023.00117(1329-1341)Online publication date: May-2023
https://doi.org/10.1109/ICSE48619.2023.00117
Wang CWang WYao PShi QZhou JXiao XZhang C(2022) Anchor: Fast and Precise Value-flow Analysis for Containers via Memory OrientationACM Transactions on Software Engineering and Methodology10.1145/356580032:3(1-39)Online publication date: 4-Oct-2022
https://dl.acm.org/doi/10.1145/3565800
Fan HLiu WHe FLee JAgrawal KSpear M(2022)Interference relation-guided SMT solving for multi-threaded program verificationProceedings of the 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming10.1145/3503221.3508424(163-176)Online publication date: 2-Apr-2022
https://dl.acm.org/doi/10.1145/3503221.3508424
Shuai ZChen ZZhang YSun JWang JCadar CZhang X(2021)Type and interval aware array constraint solving for symbolic executionProceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3460319.3464826(361-373)Online publication date: 11-Jul-2021
https://dl.acm.org/doi/10.1145/3460319.3464826
Shi QYao PWu RZhang CFreund SYahav E(2021)Path-sensitive sparse analysis without path conditionsProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454086(930-943)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454086
Xu DLiu BFeng WMing JZheng QLi JYu QFreund SYahav E(2021)Boosting SMT solver performance on mixed-bitwise-arithmetic expressionsProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454068(651-664)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454068
Chen JHe F(2021)Leveraging Control Flow Knowledge in SMT Solving of Program VerificationACM Transactions on Software Engineering and Methodology10.1145/344621130:4(1-26)Online publication date: 10-May-2021
https://dl.acm.org/doi/10.1145/3446211
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents