ESOP 2015
Tue 14 - Thu 16 April 2015 London, United Kingdom
Thu 16 Apr 2015 14:00 - 14:30 at Skeel - Session 8 Chair(s): Jan Vitek

This paper shows that it is possible to reason about the safety and termination of programs handling potentially
cyclic, singly-linked lists using propositional reasoning even when the safety invariants and termination arguments depend on constraints over the lengths of lists. For this purpose, we propose the theory SLH of singly-linked lists with length, which is able to capture non-trivial interactions between shape and arithmetic. When using the theory of bit-vector arithmetic as a background, SLH is efficiently decidable via a reduction to SAT. We show the utility of SLH for software verification by using it to express safety invariants and termination arguments for programs manipulating potentially cyclic, singly-linked lists with unrestricted, unspecified sharing. We also provide an implementation of the decision procedure and use it to check safety and termination proofs for several heap-manipulating programs.

Thu 16 Apr
Times are displayed in time zone: (GMT) Azores change

14:00 - 16:00: ESOP - Session 8 at Skeel
Chair(s): Jan VitekNortheastern University
esop-2015-papers14:00 - 14:30
Cristina DavidUniversity of Oxford, Daniel KroeningUniversity of Oxford, Matt LewisUniversity of Oxford
esop-2015-papers14:30 - 15:00
esop-2015-papers15:00 - 15:30
Azalea RaadImperial College London, Jules VillardImperial College London, Philippa GardnerImperial College London
esop-2015-papers15:30 - 16:00
Filip SieczkowskiAarhus University, Kasper SvendsenAarhus University, Lars BirkedalAarhus University, Jean Pichon-PharabodUniversity of Cambridge