Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

ESOP

2006

Springer

2006

Springer

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

Related Content

Added |
22 Aug 2010 |

Updated |
22 Aug 2010 |

Type |
Conference |

Year |
2006 |

Where |
ESOP |

Authors |
Limin Jia, David Walker |

Comments (0)