ILC: A Foundation for Automated Reasoning About Pointer Programs

13 years 10 months ago
ILC: A Foundation for Automated Reasoning About Pointer Programs
This paper presents a new program logic designed for facilitating automated reasoning about pointer programs. The program logic is directly inspired by previous work by O'Hearn, Reynolds, and Yang on separation logic, but rather than using classical bunched logic as the basis for assertions, we use Girard's intuitionistic linear logic extended with a sublogic for classical logic reasoning about arithmetic. The main contributions of the paper include the definition of a sequent calculus for our new logic, which we call ILC (Intuitionistic Linear logic with Classical arithmetic) and proof of a cut elimination. We also give a store semantics for the logic. Next, we define a simple imperative programming language with mutable references and give verification condition generation rules that produce assertions in ILC. We have proven verification condition generation is sound. Finally, we identify a fragment of ILC, ILC-, that is both decidable and closed under generation of verifi...
Limin Jia, David Walker
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where ESOP
Authors Limin Jia, David Walker
Comments (0)