ILC: A foundation for automated reasoning about pointer programs

Limin Jia, David Walker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationProgramming 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
EditorsPeter Sestoft
PublisherSpringer Verlag
Pages131-145
Number of pages15
ISBN (Print)354033095X, 9783540330950
DOIs
StatePublished - Jan 1 2006
Event15th European Symposium on Programming, ESOP 2006. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006 - Vienna, Austria
Duration: Mar 27 2006Mar 28 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3924 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other15th European Symposium on Programming, ESOP 2006. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006
Country/TerritoryAustria
CityVienna
Period3/27/063/28/06

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'ILC: A foundation for automated reasoning about pointer programs'. Together they form a unique fingerprint.

Cite this