Invariant patterns for program reasoning

Andrew Ireland, William James Ellis, Tommy Ingulfsen

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

5 Citations (Scopus)


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
Number of pages12
ISBN (Electronic)978-3-540-24694-7
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
ISSN (Print)0302-9743


ConferenceThird Mexican International Conference on Artificial Intelligence
CityMexico City


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

Cite this