Relational Symbolic Execution
By Gian Pietro Farina, Stephen Chong, Marco Gaboardi. 2017
31 citations recorded by the source corpus.
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.
Subfields: Artificial Intelligence, Software, Signal Processing
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
- Guanhong Wang
- Yuxin Wang
- Zeyu Ding
- Danfeng Zhang
- Daniel Kifer
- Ashwin Machanavajjhala
- Kamalika Chaudhuri
- Adam D. Smith
In Signal Processing
Citations in the corpus
- Detecting Violations of Differential Privacy (2018, background): “of our knowledge, this is the first paper that treats the problem of detecting counterexamples in incorrect implementations of differential privacy. Although recentwork onrelational symbolic execution[22] aims for simpler versions of this task (like detecting incorrect calculations of sensitivity), ”
- Proving differential privacy with shadow execution (2019, background): “This appears to be an important property in light of recent work on detecting counterexamples for buggy programs [12, 17, 23, 24].”