Talk "On the correctness of Symbolic Execution"

by Marcello Bonsangue

Thu, 16 January 2020 at 02:40 pm in Massa Marittima, Italy

Joint work with: Frank de Boer

Abstract: In this talk, I will discuss a formal definition of symbolic execution in terms of a symbolic transition system and prove its correctness with respect to an operational semantics which models the execution on concrete values. The approach is modular: I will first introduce such a formal model for a basic programming language with a statically fixed number of programming variables. This model is extended to a programming language with recursive procedures which are called by a call-by-value parameter mechanism. Finally, I will show how to extend this latter model of symbolic execution to arrays and object-oriented languages which feature dynamically allocated variables. If time allows, I will discuss how partial order reduction can be combined with symbolic execution in a model of multithreaded shared variable programs.