ILC: A foundation for automated reasoning about pointer programs

8Citations
Citations of this article
7Readers
Mendeley users who have this article in their library.

This artice is free to access.

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. © Springer-Verlag Berlin Heidelberg 2006.

Cite

CITATION STYLE

APA

Jia, L., & Walker, D. (2006). ILC: A foundation for automated reasoning about pointer programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3924 LNCS, pp. 131–145). Springer Verlag. https://doi.org/10.1007/11693024_10

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free