Marcello Bonsangue

Leiden University and CWI Amsterdam, The Netherlands

(invited speaker at the joint event FROM 2019 – Working Formal Methods Symposium)

 Title:  On the Nature of Symbolic Execution

Symbolic execution plays a crucial role in modern testing techniques, debugging, and automated program analysis. In particular, it is used for generating test cases. Instead of executing a program with concrete values, symbolic execution uses abstract symbols. Execution is performed by maintaining the current symbolic state together with appropriate

Although symbolic execution techniques have improved enormously in the last few years with application in several software analysis tools, not much effort has been spent on its formal justification. In this talk, based on a join effort with Frank de Boer, we introduce a formal model of symbolic execution for a basic programming language and show its correctness.

We show how to extend the basic theory to more advanced programming concepts, such as recursive procedures, object-orientation, arrays, multithreading, and concurrent objects, and conclude with some of the challenges and possibilities of a formal approach to symbolic execution.