Cited By
View all- Lu SBodík R(2023)Grisette: Symbolic Compilation as a Functional Programming LibraryProceedings of the ACM on Programming Languages10.1145/35712097:POPL(455-487)Online publication date: 9-Jan-2023
From definitional interpreter to symbolic executor
Authors: 
Adrian D. Mensing, Hendrik van Antwerpen, 
Casper Bach Poulsen, 
Eelco VisserAuthors Info & Claims
Pages 11 - 20
Abstract
Symbolic execution is a technique for automatic software validation and verification. New symbolic executors regularly appear for both existing and new languages and such symbolic executors are generally manually (re)implemented each time we want to support a new language. We propose to automatically generate symbolic executors from language definitions, and present a technique for mechanically (but as yet, manually) deriving a symbolic executor from a definitional interpreter. The idea is that language designers define their language as a monadic definitional interpreter, where the monad of the interpreter defines the meaning of branch points. Developing a symbolic executor for a language is a matter of changing the monadic interpretation of branch points. In this paper, we illustrate the technique on a language with recursive functions and pattern matching, and use the derived symbolic executor to automatically generate test cases for definitional interpreters implemented in our defined language.
References
[1]
Saswat Anand, Corina S. Pasareanu, and Willem Visser. 2007. JPF-SE: A Symbolic Execution Extension to Java PathFinder. In Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings (Lecture Notes in Computer Science), Orna Grumberg and Michael Huth (Eds.), Vol. 4424. Springer, 134-138.
[2]
Shay Artzi, Adam Kiezun, Julian Dolby, Frank Tip, Danny Dig, Amit M. Paradkar, and Michael D. Ernst. 2010. Finding Bugs in Web Applications Using Dynamic Test Generation and Explicit-State Model Checking. IEEE Trans. Software Eng. 36, 4 (2010), 474-494.
[3]
Stefan Bucur, Johannes Kinder, and George Candea. 2014. Prototyping symbolic execution engines for interpreted languages. In Architectural Support for Programming Languages and Operating Systems, ASPLOS '14, Salt Lake City, UT, USA, March 1-5, 2014, Rajeev Balasubramonian, Al Davis, and Sarita V. Adve (Eds.). ACM, 239-254.
[4]
Jacob Burnim and Koushik Sen. 2008. Heuristics for Scalable Dynamic Test Generation. In 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), 15-19 September 2008, L'Aquila, Italy. IEEE Computer Society, 443-446.
[5]
William E. Byrd. 2010. Relational Programming in miniKanren: Techniques, Applications, and Implementations. Ph.D. Dissertation. Indiana University.
[6]
William E. Byrd, Michael Ballantyne, Gregory Rosenblatt, and Matthew Might. 2017. A unified approach to solving seven programming problems (functional pearl). PACMPL 1, ICFP (2017), 8:1-8:26.
[7]
William E. Byrd and Daniel P. Friedman. 2006. From Variadic Functions to Variadic Relations: A miniKanren Perspective. In Proceedings of the 2006 Scheme and Functional Programming Workshop. http://scheme2006.cs.uchicago.edu/12-byrd.pdf
[8]
William E. Byrd, Eric Holk, and Daniel P. Friedman. 2012. miniKanren, live and untagged: quine generation via relational interpreters (programming pearl). In Proceedings of the 2012 Annual Workshop on Scheme and Functional Programming, Scheme 2012, Copenhagen, Denmark, September 9-15, 2012, Olivier Danvy (Ed.). ACM, 8-29.
[9]
Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings, Richard Draves and Robbert van Renesse (Eds.). USENIX Association, 209-224. http://www.usenix.org/events/osdi08/tech/full_papers/cadar/cadar.pdf
[10]
Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan. 2009. Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. J. Funct. Program. 19, 5 (2009), 509-543.
[11]
Patrick Cousot. [n.d.]. Symbolic Execution is a case of Abstract Interpretation? Theoretical Computer Science Stack Exchange. https://cstheory.stackexchange.com/q/42290
[12]
Patrick Cousot. 1978. Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique des programmes. https://tel.archives-ouvertes.fr/tel-00288657
[13]
Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, Robert M. Graham, Michael A. Harrison, and Ravi Sethi (Eds.). ACM, 238-252.
[14]
Shingo Eguchi, Naoki Kobayashi, and Takeshi Tsukada. 2018. Automated Synthesis of Functional Programs with Auxiliary Functions. In Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings (Lecture Notes in Computer Science), Sukyoung Ryu (Ed.), Vol. 11275. Springer, 223-241.
[15]
Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Shriram Krishnamurthi, Eli Barzilay, Jay A. McCarthy, and Sam Tobin-Hochstadt. 2015. The Racket Manifesto. In 1st Summit on Advances in Programming Languages, SNAPL 2015, May 3-6, 2015, Asilomar, California, USA (LIPIcs), Thomas Ball, Rastislav Bodík, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett (Eds.), Vol. 32. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 113-128.
[16]
Daniel P. Friedman, William E. Byrd, and Oleg Kiselyov. 2005. The reasoned schemer. MIT Press.
[17]
Aggelos Giantsios, Nikolaos Papaspyrou, and Konstantinos Sagonas. 2017. Concolic testing for functional languages. Sci. Comput. Program. 147 (2017), 109-134.
[18]
Andy Gill. 2019. The Monad Transformer Library. http://hackage.haskell.org/package/mtl-2.2.2/
[19]
Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: directed automated random testing. In Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, June 12-15, 2005, Vivek Sarkar and Mary W. Hall (Eds.). ACM, 213-223.
[20]
Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. 2017. Program Synthesis. Foundations and Trends in Programming Languages 4, 1-2 (2017), 1-119.
[21]
Peter Hancock and Anton Setzer. 2000. Interactive Programs in Dependent Type Theory. In Computer Science Logic, 14th Annual Conference of the EACSL, Fischbachau, Germany, August 21-26, 2000, Proceedings (Lecture Notes in Computer Science), Peter Clote and Helmut Schwichtenberg (Eds.), Vol. 1862. Springer, 317-331.
[22]
Jason Hemann and Daniel P. Friedman. 2013. μKanren: A Minimal Functional Core for Relational Programming. In Proceedings of the 2013 Workshop on Scheme and Functional Programming (Scheme'13).
[23]
Christian Hofer, Klaus Ostermann, Tillmann Rendel, and Adriaan Moors. 2008. Polymorphic Embedding of DSLs. In Generative Programming and Component Engineering, 7th International Conference, GPCE 2008, Nashville, TN, USA, October 19-23, 2008, Proceedings, Yannis Smaragdakis and Jeremy G. Siek (Eds.). ACM, 137-148.
[24]
Mark P. Jones. 1995. Functional Programming with Overloading and Higher-Order Polymorphism. In Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques, Båstad, Sweden, May 24-30, 1995, Tutorial Text (Lecture Notes in Computer Science), Johan Jeuring and Erik Meijer (Eds.), Vol. 925. Springer, 97-136.
[25]
Lennart C. L. Kats and Eelco Visser. 2010. The spoofax language workbench: rules for declarative specification of languages and IDEs. In Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2010, October 17-21, 2010, Reno/Tahoe, Nevada, USA, William R. Cook, Siobhán Clarke, and Martin C. Rinard (Eds.). ACM, 444-463.
[26]
Sven Keidel, Casper Bach Poulsen, and Sebastian Erdweg. 2018. Compositional soundness proofs of abstract interpreters. PACMPL 2, ICFP (2018), 72:1-72:26.
[27]
James C. King. 1976. Symbolic Execution and Program Testing. Commun. ACM 19, 7 (1976), 385-394.
[28]
Oleg Kiselyov and Hiromi Ishii. 2015. Freer monads, more extensible effects. In Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015, Vancouver, BC, Canada, September 3-4, 2015, Ben Lippmeier (Ed.). ACM, 94-105.
[29]
Paul Klint, Tijs van der Storm, and Jurgen J. Vinju. 2009. RASCAL: A Domain Specific Language for Source Code Analysis and Manipulation. In Ninth IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2009, Edmonton, Alberta, Canada, September 20-21, 2009. IEEE Computer Society, 168-177.
[30]
Dmitry Kosarev and Dmitry Boulytchev. 2016. Typed Embedding of a Relational Language in OCaml. In Proceedings ML Family Workshop / OCaml Users and Developers workshops, ML/OCAML 2016, Nara, Japan, September 22-23, 2016. (EPTCS), Kenichi Asai and Mark R. Shinwell (Eds.), Vol. 285. 1-22.
[31]
Guodong Li, Indradeep Ghosh, and Sreeranga P. Rajan. 2011. KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings (Lecture Notes in Computer Science), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.), Vol. 6806. Springer, 609-615.
[32]
Sheng Liang, Paul Hudak, and Mark P. Jones. 1995. Monad Transformers and Modular Interpreters. In Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995, Ron K. Cytron and Peter Lee (Eds.). ACM Press, 333-343.
[33]
Marcus Lindner, Jorge Aparicius, and Per Lindgren. 2018. No Panic! Verification of Rust Programs by Symbolic Execution. In 16th IEEE International Conference on Industrial Informatics, INDIN 2018, Porto, Portugal, July 18-20, 2018. IEEE, 108-114.
[34]
Kuang-Chen Lu, Weixi Ma, and Daniel P. Friedman. 2019. Towards a miniKanren with fair search strategies. In Proceedings of the Workshop on miniKanren 2019, Berlin, Germany. http://minikanren.org/workshop/2019/minikanren19-final1.pdf
[35]
Peter-Michael Osera and Steve Zdancewic. 2015. Type-and-example-directed program synthesis. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, David Grove and Steve Blackburn (Eds.). ACM, 619-630.
[36]
Dmitry Rozplokhas, Andrey Vyatkin, and Dmitri Boulytchev. 2019. Certified Semantics for miniKanren. In Proceedings of the Workshop on miniKanren 2019, Berlin, Germany. http://minikanren.org/workshop/2019/minikanren19-final5.pdf
[37]
Koushik Sen and Gul Agha. 2006. CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools. In Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings (Lecture Notes in Computer Science), Thomas Ball and Robert B. Jones (Eds.), Vol. 4144. Springer, 419-423.
[38]
Koushik Sen, Darko Marinov, and Gul Agha. 2005. CUTE: a concolic unit testing engine for C. In Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2005, Lisbon, Portugal, September 5-9, 2005, Michel Wermelinger and Harald C. Gall (Eds.). ACM, 263-272.
[39]
Wouter Swierstra and Tim Baanen. 2019. A Predicate Transformer Semantics for Effects. PACMPL ICFP (2019).
[40]
Emina Torlak and Rastislav Bodík. 2013. Growing solver-aided languages with rosette. In ACM Symposium on New Ideas in Programming and Reflections on Software, Onward! 2013, part of SPLASH '13, Indianapolis, IN, USA, October 26-31, 2013, Antony L. Hosking, Patrick Th. Eugster, and Robert Hirschfeld (Eds.). ACM, 135-152.
[41]
Emina Torlak and Rastislav Bodík. 2014. A lightweight symbolic virtual machine for solver-aided host languages. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '14, Edinburgh, United Kingdom - June 09 - 11, 2014, Michael F. P. O'Boyle and Keshav Pingali (Eds.). ACM, 530-541.
Index Terms
- From definitional interpreter to symbolic executor
Recommendations
Layout-sensitive language extensibility with SugarHaskell
Haskell '12: Proceedings of the 2012 Haskell SymposiumProgrammers need convenient syntax to write elegant and concise programs. Consequently, the Haskell standard provides syntactic sugar for some scenarios (e.g., do notation for monadic code), authors of Haskell compilers provide syntactic sugar for more ...
Effect handlers in scope
Haskell '14Algebraic effect handlers are a powerful means for describing effectful computations. They provide a lightweight and orthogonal technique to define and compose the syntax and semantics of different effects. The semantics is captured by handlers, which ...
Symbolic types for lenient symbolic execution
We present lambda_sym, a typed λ-calculus for lenient symbolic execution, where some language constructs do not recognize symbolic values. Its type system, however, ensures safe behavior of all symbolic values in a program. Our calculus extends a base ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2019
39 pages
Copyright © 2019 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 20 October 2019
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
SPLASH '19
Sponsor:
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 166Total Downloads
- Downloads (Last 12 months)14
- Downloads (Last 6 weeks)0
Reflects downloads up to 18 Nov 2024
Other Metrics
Citations
Cited By
View all- Lu SBodík R(2023)Grisette: Symbolic Compilation as a Functional Programming LibraryProceedings of the ACM on Programming Languages10.1145/35712097:POPL(455-487)Online publication date: 9-Jan-2023
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in