Sciweavers

APLAS
2005
ACM
13 years 10 months ago
Symbolic Execution with Separation Logic
We describe a sound method for automatically proving Hoare triples for loop-free code in Separation Logic, for certain preconditions and postconditions (symbolic heaps). The method...
Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn