Relational symbolic execution
Files
Accepted manuscript
Date
2019-10-07
Authors
Farina, Gian Pietro
Chong, Stephen
Gaboardi, Marco
Version
Accepted manuscript
OA Version
Citation
Gian Pietro Farina, Stephen Chong, Marco Gaboardi. 2019. "Relational Symbolic Execution." Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages 2019, https://doi.org/10.1145/3354166.3354175
Abstract
Symbolic execution is a classical program analysis technique used to show that programs satisfy or violate given specifications. In this work we generalize symbolic execution to support program analysis for relational specifications in the form of relational properties - these are properties about two runs of two programs on related inputs, or about two executions of a single program on related inputs. Relational properties are useful to formalize notions in security and privacy, and to reason about program optimizations. We design a relational symbolic execution engine, named RelSym which supports interactive refutation, as well as proving of relational properties for programs written in a language with arrays and for-like loops.