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...

• Type: Conference
• Year: 2006
• Where: ESOP
• Authors: Limin Jia, David Walker
• Keywords: ESOP 2006, Intuitionistic Linear Logic, Logic, Programming Languages, Verification Condition