Invariant patterns for program reasoning

Andrew Ireland, William James Ellis, Tommy Ingulfsen

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

5 Citations (Scopus)

Abstract

We address the problem of integrating standard techniques for automatic invariant generation within the context of program reasoning. We propose the use of invariant patterns which enable us to associate common patterns of program code and specifications with invariant schemas. This allows crucial decisions relating to the development of invariants to be delayed until a proof is attempted. Moreover, it allows patterns within the program to be exploited in patching failed proof attempts.

Original languageEnglish
Title of host publicationMICAI 2004: Advances in Artificial Intelligence
Subtitle of host publicationThird Mexican International Conference on Artificial Intelligence, Mexico City, Mexico, April 26-30, 2004. Proceedings
Pages190-201
Number of pages12
Volume2972
ISBN (Electronic)978-3-540-24694-7
DOIs
Publication statusPublished - 2004
EventThird Mexican International Conference on Artificial Intelligence - Mexico City, Mexico
Duration: 26 Apr 200430 Apr 2004

Publication series

NameLecture Notes in Computer Science
Volume2972
ISSN (Print)0302-9743

Conference

ConferenceThird Mexican International Conference on Artificial Intelligence
CountryMexico
CityMexico City
Period26/04/0430/04/04

Fingerprint Dive into the research topics of 'Invariant patterns for program reasoning'. Together they form a unique fingerprint.

  • Cite this

    Ireland, A., Ellis, W. J., & Ingulfsen, T. (2004). Invariant patterns for program reasoning. In MICAI 2004: Advances in Artificial Intelligence: Third Mexican International Conference on Artificial Intelligence, Mexico City, Mexico, April 26-30, 2004. Proceedings (Vol. 2972, pp. 190-201). (Lecture Notes in Computer Science; Vol. 2972). https://doi.org/10.1007/978-3-540-24694-7_20