Symbolic Execution with Separation Logic
By Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn. Asian Symposium on Programming Languages and Systems, 2005
370 citations recorded by the source corpus.
Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software
View Paper: https://www.semanticscholar.org/paper/765133e5c7375c7160ecaf0d9d1b398f3299e886
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
- Matthew J. Parkinson
- Viktor Vafeiadis
- Cristiano Calcagno
- Peter W. O'Hearn
- Hongseok Yang
- Josh Berdine
- Dino Distefano
- S. Brookes
In Computational Theory and Mathematics
- Matthew J. Parkinson
- Viktor Vafeiadis
- Cristiano Calcagno
- Peter W. O'Hearn
- Hongseok Yang
- Josh Berdine
- Dino Distefano
- S. Brookes
In Software
- Matthew J. Parkinson
- Viktor Vafeiadis
- Peter W. O'Hearn
- Cristiano Calcagno
- Josh Berdine
- Dino Distefano
- Hongseok Yang
Citations in the corpus
- A Local Shape Analysis Based on Separation Logic (2006, background): “They also utilize a symbolic execution mechanism related to [5], and give rewrite rules to attempt to find fixed points.”
- Smallfoot: Modular Automatic Assertion Checking with Separation Logic (2005, methodology): “Smallfoot chops an annotated program into Hoare triples for certain symbolic instructions, that are then decided using the symbolic execution mechanism of [5].”
- A Marriage of Rely/Guarantee and Separation Logic (2007, methodology): “In future work, we plan to build a tool to automate these checks by modifying Smallfoot [ 2 ], a separation logic theorem prover.”