ESOP 2015
Tue 14 - Thu 16 April 2015 London, United Kingdom
Thu 16 Apr 2015 12:00 - 12:30 at Skeel - Session 7 Chair(s): Delphine Demange

We propose SplInter, a new technique for proving safety properties of heap-manipulating programs that marries a new separation logic–based analysis for heap reasoning with an interpolation-based technique for refining and strengthening heap shape invariants with data invariants. SplInter is property-directed, precise, and produces counterexample traces in case a property does not hold. Using the novel notion of spatial interpolants modulo theories, SplInter can infer complex invariants over general recursive predicates, e.g., of the form “all data elements in a linked list are even” or “a binary tree is sorted”. Furthermore, we treat interpolation as a black box, which gives us the freedom to encode data manipulation in whatever theory is suitable for the program at hand (e.g., bitvectors, arrays, or linear arithmetic), so that our technique immediately benefits from any future advances in SMT solving and interpolation.

Thu 16 Apr

esop-2015-papers
10:30 - 12:30: ESOP - Session 7 at Skeel
Chair(s): Delphine DemangeIRISA / University of Rennes 1
esop-2015-papers10:30 - 11:00
Talk
Sam LindleyUniversity of Edinburgh, J. Garrett MorrisThe University of Edinburgh
esop-2015-papers11:00 - 11:30
Talk
Alexey GotsmanIMDEA, Hongseok YangUniversity of Oxford
esop-2015-papers11:30 - 12:00
Talk
Tachio TerauchiJAIST, Hiroshi UnnoUniversity of Tsukuba
esop-2015-papers12:00 - 12:30
Talk
Aws AlbarghouthiUniversity of Wisconsin - Madison, Josh BerdineMicrosoft Research, Byron CookMicrosoft Research, Zachary KincaidUniversity of Toronto