Document Open Access Logo

Symbolic Execution as DPLL Modulo Theories

Author Quoc-Sang Phan

PDF

File

Thumbnail PDF
PDF
OASIcs.ICCSW.2014.58.pdf
  • Filesize: 0.63 MB
  • 8 pages

Document Identifiers

Subject Classification

Keywords
  • Symbolic Execution
  • Satisfiability Modulo Theories

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We show how Symbolic Execution can be understood as a variant of the DPLL(T ) algorithm, which is the dominant technique for the Satisfiability Modulo Theories (SMT) problem. In other words, Symbolic Executors are SMT solvers. This view enables us to use an SMT solver, with the ability of generating all models with respect to a set of Boolean atoms, to explore all symbolic paths of a program. This results in a more lightweight approach for Symbolic Execution.

Cite As Get BibTex

Quoc-Sang Phan. Symbolic Execution as DPLL Modulo Theories. In 2014 Imperial College Computing Student Workshop. Open Access Series in Informatics (OASIcs), Volume 43, pp. 58-65, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014) https://doi.org/10.4230/OASIcs.ICCSW.2014.58

Author Details

Quoc-Sang Phan

References

  1. Clark Barrett, Aaron Stump, and Cesare Tinelli. The smt-lib standard: Version 2.0. In SMT Workshop, 2010. Google Scholar
  2. Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, and Roberto Sebastiani. The mathsat 4 smt solver. In Proceedings of the 20th international conference on Computer Aided Verification, CAV '08, pages 299-303, Berlin, Heidelberg, 2008. Springer-Verlag. Google Scholar
  3. Cristian Cadar, Daniel Dunbar, and Dawson Engler. Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. OSDI'08, pages 209-224. Google Scholar
  4. Cristian Cadar, Patrice Godefroid, Sarfraz Khurshid, Corina S. Păsăreanu, Koushik Sen, Nikolai Tillmann, and Willem Visser. Symbolic execution for software testing in practice: Preliminary assessment. In Proceedings of the 33rd International Conference on Software Engineering, ICSE '11, pages 1066-1071, New York, NY, USA, 2011. ACM. Google Scholar
  5. Cristian Cadar and Koushik Sen. Symbolic execution for software testing: Three decades later. Commun. ACM, 56(2):82-90, February 2013. Google Scholar
  6. R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck. An efficient method of computing static single assignment form. In Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '89, pages 25-35, New York, NY, USA, 1989. ACM. Google Scholar
  7. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Commun. ACM, 5(7):394-397, July 1962. Google Scholar
  8. Leonardo De Moura and Nikolaj Bjørner. Z3: an efficient smt solver. In Proceedings of the 14th international conference on Tools and algorithms for the construction and analysis of systems, TACAS'08, pages 337-340, Berlin, Heidelberg, 2008. Springer-Verlag. Google Scholar
  9. Leonardo De Moura and Nikolaj Bjørner. Satisfiability modulo theories: introduction and applications. Commun. ACM, 54(9):69-77, September 2011. Google Scholar
  10. Vijay Ganesh and David L. Dill. A decision procedure for bit-vectors and arrays. In Proceedings of the 19th international conference on Computer aided verification, CAV'07, pages 519-531, Berlin, Heidelberg, 2007. Springer-Verlag. Google Scholar
  11. James C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385-394, July 1976. Google Scholar
  12. Quoc-Sang Phan and Pasquale Malacaria. Abstract model counting: A novel approach for quantification of information leaks. In Proceedings of the 9th ACM Symposium on Information, Computer and Communications Security, ASIA CCS '14, pages 283-292, New York, NY, USA, 2014. ACM. Google Scholar
  13. Quoc-Sang Phan, Pasquale Malacaria, Oksana Tkachuk, and Corina S. Păsăreanu. Symbolic quantitative information flow. SIGSOFT Softw. Eng. Notes, 37(6):1-5, November 2012. Google Scholar
  14. Corina S. Păsăreanu and Neha Rungta. Symbolic pathfinder: symbolic execution of java bytecode. In Proceedings of the IEEE/ACM international conference on Automated software engineering, ASE '10, pages 179-180, New York, NY, USA, 2010. ACM. Google Scholar
  15. Roberto Sebastiani. Lazy Satisfiability Modulo Theories. Journal on Satisfiability, Boolean Modeling and Computation, 3:141-224, 2007. Google Scholar
  16. Willem Visser, Jaco Geldenhuys, and Matthew B. Dwyer. Green: reducing, reusing and recycling constraints in program analysis. In Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering, FSE '12, pages 58:1-58:11, New York, NY, USA, 2012. ACM. Google Scholar
  17. Christoph M. Wintersteiger, Youssef Hamadi, and Leonardo Mendonça de Moura. A concurrent portfolio approach to smt solving. In CAV, pages 715-720, 2009. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact