@inproceedings{8127acb0f02444fea4d5702da198d9f7,
title = "ILC: A foundation for automated reasoning about pointer programs",
abstract = "This paper shows how to use Girard's intuitionistic linear logic extended with a classical sublogic to reason about pointer programs. More specifically, first, the paper defines the proof theory for ILC (Intuitionistic Linear logic with Constraints) and shows it is well-defined via a proof of cut elimination. Second, inspired by prior work of O'Hearn, Reynolds, and Yang, the paper explains how to interpret linear logical formulas as descriptions of a program store. Third, this paper defines a simple imperative programming language with mutable references and arrays and gives verification condition generation rules that produce assertions in ILC. Finally, we identify a fragment of ILC, ILC -, that is both decidable and closed under generation of verification conditions. Since verification condition generation is syntax-directed, we obtain a decidable procedure for checking properties of pointer programs.",
author = "Limin Jia and David Walker",
year = "2006",
month = jan,
day = "1",
doi = "10.1007/11693024_10",
language = "English (US)",
isbn = "354033095X",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "131--145",
editor = "Peter Sestoft",
booktitle = "Programming Languages and Systems - 15th European Symposium on Programming, ESOP 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Proceedings",
address = "Germany",
note = "15th European Symposium on Programming, ESOP 2006. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006 ; Conference date: 27-03-2006 Through 28-03-2006",
}