Write a Blog >>
Sun 20 - Fri 25 October 2019 Athens, Greece
Sun 20 Oct 2019 09:30 - 10:00 at Room 1A - Model and Theory Chair(s): Guido Chari

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 of 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. Our long-term goal is to integrate these techniques in language development workbenches and workflows, to make developer-boosting meta-programming techniques such as symbolic execution readily and automatically available to language designers and software developers. 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.

Sun 20 Oct
Times are displayed in time zone: Beirut change

09:00 - 10:30: Model and TheoryMETA at Room 1A
Chair(s): Guido ChariCzech Technical University
09:00 - 09:30
Ambiguous, Informal, and Unsound: Metaprogramming for Naturalness
Toni MattisHasso Plattner Institute, University of Potsdam, Patrick ReinHasso Plattner Institute, Germany, Robert HirschfeldHasso-Plattner-Institut (HPI), Germany
09:30 - 10:00
From Definitional Interpreter To Symbolic Executor
Adrian Mensing, Hendrik van AntwerpenTU Delft, Eelco VisserDelft University of Technology, Casper Bach PoulsenDelft University of Technology
Link to publication Pre-print
10:00 - 10:30
Mμl: The Power of Dynamic Multi-Methods
Isaac Oscar GarianoVictoria University of Wellington, Marco ServettoVictoria University Wellington, New Zealand
File Attached