Document Open Access Logo

Abstract Interpretation, Symbolic Execution and Constraints

Authors Roberto Amadini , Graeme Gange , Peter Schachte , Harald Søndergaard , Peter J. Stuckey

PDF
Thumbnail PDF

File

OASIcs.Gabbrielli.7.pdf
  • Filesize: 0.49 MB
  • 19 pages

Document Identifiers

Author Details

Roberto Amadini
  • University of Bologna, Italy
Graeme Gange
  • Monash University, Clayton, Australia
Peter Schachte
  • The University of Melbourne, Australia
Harald Søndergaard
  • The University of Melbourne, Australia
Peter J. Stuckey
  • Monash University, Clayton, Australia

Acknowledgements

We wish to thank the anonymous reviewers for their detailed and constructive suggestions.

Cite AsGet BibTex

Roberto Amadini, Graeme Gange, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. Abstract Interpretation, Symbolic Execution and Constraints. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/OASIcs.Gabbrielli.7

Abstract

Abstract interpretation is a static analysis framework for sound over-approximation of all possible runtime states of a program. Symbolic execution is a framework for reachability analysis which tries to explore all possible execution paths of a program. A shared feature between abstract interpretation and symbolic execution is that each - implicitly or explicitly - maintains constraints during execution, in the form of invariants or path conditions. We investigate the relations between the worlds of abstract interpretation, symbolic execution and constraint solving, to expose potential synergies.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program analysis
  • Theory of computation → Invariants
  • Software and its engineering → Software maintenance tools
  • Software and its engineering → Software testing and debugging
Keywords
  • Abstract interpretation
  • symbolic execution
  • constraint solving
  • dynamic analysis
  • static analysis

Metrics

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

References

  1. W. Ahrendt, B. Beckert, R. Bubel, R. Hähnle, P. H. Schmitt, and M. Ulbrich, editors. Dedecutive Software Verification - The KeY Book, volume 10001 of Lecture Notes in Computer Science. Springer, 2016. Google Scholar
  2. Eman Alatawi, Harald Søndergaard, and Tim Miller. Leveraging abstract interpretation for efficient dynamic symbolic execution. In G. Rosu, M. Di Penta, and T. N. Nguyen, editors, Proc. 32nd IEEE/ACM Int. Conf. Automated Software Engineering, pages 619-624. IEEE Comp. Soc., 2017. Google Scholar
  3. Roberto Amadini, Graeme Gange, Peter J. Stuckey, and Guido Tack. A novel approach to string constraint solving. In J. C. Beck, editor, Proc. 23rd Int. Conf. Principles and Practice of Constraint Programming, volume 10416 of Lecture Notes in Computer Science, pages 3-20. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66158-2_1.
  4. Roberto Baldoni, Emilio Coppa, Daniele Cono D'Elia, Camil Demetrescu, and Irene Finocchi. A survey of symbolic execution techniques. ACM Computing Surveys, 51(3):50:1-50:39, 2018. Google Scholar
  5. Thomas Ball. The concept of dynamic analysis. In O. Nierstrasz and M. Lemoine, editors, Software Engineering - ESEC/FSE'99, volume 1687 of Lecture Notes in Computer Science, pages 216-234. Springer, 1999. Google Scholar
  6. Bernhard Beckert, Vladimir Klebanov, and Benjamin Weiß. Dynamic logic for Java. In Deductive Software Verification - The KeY Book, volume 10001 of Lecture Notes in Computer Science, pages 49-106. Springer, 2016. Google Scholar
  7. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009. Google Scholar
  8. Robert S. Boyer, Bernard Elspas, and Karl N. Levitt. SELECT: A formal system for testing and debugging programs by symbolic execution. ACM SIGPLAN Notices, 10(6):234-245, 1975. Google Scholar
  9. R. M. Burstall. Program proving as hand simulation with a little induction. In Information Processing: Proc. IFIP Congress 1974, pages 308-314. North-Holland, 1974. Google Scholar
  10. Cristian Cadar, Daniel Dunbar, and Dawson Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proc. 8th USENIX Conf. Operating Systems Design and Implementation, volume 8, pages 209-224, 2008. Google Scholar
  11. Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In E. Allen Emerson and A. Prasad Sistla, editors, Computer Aided Verification: Proc. 12th Int. Conf., volume 1855 of Lecture Notes in Computer Science, pages 154-169. Springer, 2000. Google Scholar
  12. Agostino Cortesi and Matteo Zanioli. Widening and narrowing operators for abstract interpretation. Computer Languages, Systems and Structures, 37(1):24-42, 2011. Google Scholar
  13. Giulia Costantini, Pietro Ferrara, and Agostino Cortesi. A suite of abstract domains for static analysis of string values. Software Practice and Experience, 45(2):245-287, 2015. Google Scholar
  14. Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. 4th ACM Symp. Principles of Programming Languages (POPL'77), pages 238-252. ACM, 1977. Google Scholar
  15. Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. In Proc. 6th ACM SIGACT-SIGPLAN Symp. Principles of Programming Languages (POPL'79), pages 269-282. ACM, 1979. Google Scholar
  16. Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear constraints among variables of a program. In Proc. Fifth ACM Symp. Principles of Programming Languages (POPL'78), pages 84-97. ACM, 1978. Google Scholar
  17. George B. Dantzig. Linear programming. Operations Research, 50(1):42-47, 2002. Google Scholar
  18. Josselin Feist, Laurent Mounier, Marie-Laure Potet, Sébastien Bardin, and Robin David. Finding the needle in the heap: Combining static analysis and dynamic symbolic execution to trigger use-after-free. In Proceedings of the 6th ACM Workshop on Software Security, Protection, and Reverse Engineering, pages 2:1-2:12. ACM, 2016. Google Scholar
  19. Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. Abstract interpretation over non-lattice abstract domains. In F. Logozzo and M. Fähndrich, editors, Static Analysis, volume 7935 of Lecture Notes in Computer Science, pages 6-24. Springer, 2013. Google Scholar
  20. Patrice Godefroid, Nils Klarlund, and Koushik Sen. DART: Directed automated random testing. In Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI'05), pages 213-223. ACM, 2005. URL: https://doi.org/10.1145/1065010.1065036.
  21. Patrice Godefroid and Daniel Luchaup. Automatic partial loop summarization in dynamic test generation. In Proc. 2011 Int. Symp. Software Testing and Analysis (ISSTA'11), pages 23-33. ACM, 2011. URL: https://doi.org/10.1145/2001420.2001424.
  22. Philippe Granger. Static analysis of linear congruence equalities among variables of a program. In Samson Abramsky and T. S. E. Maibaum, editors, TAPSOFT'91: Proc. Int. Joint Conf. Theory and Practice of Software Development, Volume 1: Colloquium on Trees in Algebra and Programming (CAAP'91), volume 493 of Lecture Notes in Computer Science, pages 169-192. Springer, 1991. Google Scholar
  23. Mark Harman, Lin Hu, Rob Hierons, Joachim Wegener, Harmen Sthamer, André Baresel, and Marc Roper. Testability transformation. IEEE Transactions on Software Engineering, 30(1):3-16, 2004. Google Scholar
  24. Bart Jacobs, Jan Smans, and Frank Piessens. A quick tour of the VeriFast program verifier. In K. Ueda, editor, Programming Languages and Systems: Proc. 8th Asian Symp., volume 6461 of Lecture Notes in Computer Science, pages 304-311. Springer, 2010. Google Scholar
  25. James C. King. Symbolic execution and program testing. Communications of the ACM, 19(7):385-394, 1976. Google Scholar
  26. Jean-Louis Laurière. A language and a program for stating and solving combinatorial problems. Artificial Intellgence, 10(1):29-127, 1978. Google Scholar
  27. Antoine Miné. The Octagon abstract domain. Higher-Order and Symbolic Computation, 19(1):31-100, 2006. Google Scholar
  28. Ugo Montanari. Networks of constraints: Fundamental properties and applications to picture processing. Information Sciences, 7:95-132, 1974. Google Scholar
  29. Sebastian Poeplau and Aurélien Francillon. Symbolic execution with SymCC: Don't interpret, compile! In Proc. 2020 USENIX Security Symp. USENIX, 2020. Could not find this on the USENIX Security 20 web site. Google Scholar
  30. Olivier Ponsini, Claude Michel, and Michel Rueher. Verifying floating-point programs with constraint programming and abstract interpretation techniques. Automated Software Engineering, 23(2):191-217, 2016. Google Scholar
  31. F. Rossi, P. van Beek, and T. Walsh, editors. Handbook of Constraint Programming. Elsevier, 2006. Google Scholar
  32. Prateek Saxena, Pongsin Poosankam, Stephen McCamant, and Dawn Song. Loop-extended symbolic execution on binary programs. In Proc. 18th Int. Symp. Software Testing and Analysis (ISSTA'09), pages 225-236. ACM, 2009. URL: https://doi.org/10.1145/1572272.1572299.
  33. Koushik Sen and Gul Agha. CUTE and jCUTE: Concolic unit testing and explicit path model-checking tools. In T. Ball and R. B. Jones, editors, Computer Aided Verification: Proc. 18th Int. Conf., volume 4144 of Lecture Notes in Computer Science, pages 419-423. Springer, 2006. Google Scholar
  34. Koushik Sen, Darko Marinov, and Gul Agha. CUTE: A concolic unit testing engine for C. In Proc. 10th European Software Engineering Conf., pages 263-272. ACM, 2005. URL: https://doi.org/10.1145/1081706.1081750.
  35. Bhargava Shastry, Markus Leutner, Tobias Fiebig, Kashyap Thimmaraju, Fabian Yamaguchi, Konrad Rieck, Stefan Schmid, Jean-Pierre Seifert, and Anja Feldmann. Static program analysis as a fuzzing aid. In M. Dacier, M. Bailey, M. Polychronakis, and M. Antonakakis, editors, Research in Attacks, Intrusions, and Defenses: Proc. 20th Int. Symp. (RAID'17), volume 10453 of Lecture Notes in Computer Science, pages 26-47. Springer, 2017. Google Scholar
  36. Arnaud J. Venet. The Gauge domain: Scalable analysis of linear inequality invariants. In P. Madushan and S. A. Seshia, editors, Computer Aided Verification, volume 7358 of Lecture Notes in Computer Science, pages 139-154. Springer, 2012. Google Scholar
  37. Nathan Wasser, Reiner Hähnle, and Richard Bubel. Abstract interpretation. In Deductive Software Verification - The KeY Book, volume 10001 of Lecture Notes in Computer Science, pages 167-189. Springer, 2016. Google Scholar
  38. Insu Yun, Sangho Lee, Meng Xu, Yeongjin Jang, and Taesoo Kim. QSYM: A practical concolic execution engine tailored for hybrid fuzzing. In Proc. 27th USENIX Security Symp., pages 745-761. USENIX, 2018. 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact