Invariant patterns for program reasoning

Andrew Ireland; William James Ellis; Tommy Ingulfsen

doi:10.1007/978-3-540-24694-7_20

Invariant patterns for program reasoning

Andrew Ireland, William James Ellis, Tommy Ingulfsen

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

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 language	English
Title of host publication	MICAI 2004: Advances in Artificial Intelligence
Subtitle of host publication	Third Mexican International Conference on Artificial Intelligence, Mexico City, Mexico, April 26-30, 2004. Proceedings
Pages	190-201
Number of pages	12
Volume	2972
ISBN (Electronic)	978-3-540-24694-7
DOIs	https://doi.org/10.1007/978-3-540-24694-7_20
Publication status	Published - 2004
Event	Third Mexican International Conference on Artificial Intelligence - Mexico City, Mexico Duration: 26 Apr 2004 → 30 Apr 2004

Publication series

Name	Lecture Notes in Computer Science
Volume	2972
ISSN (Print)	0302-9743

Conference

Conference	Third Mexican International Conference on Artificial Intelligence
Country/Territory	Mexico
City	Mexico City
Period	26/04/04 → 30/04/04

Access to Document

10.1007/978-3-540-24694-7_20

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

@inbook{53741acd86fb43fabc94aadf62533acd,

title = "Invariant patterns for program reasoning",

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

author = "Andrew Ireland and Ellis, {William James} and Tommy Ingulfsen",

year = "2004",

doi = "10.1007/978-3-540-24694-7_20",

language = "English",

isbn = "978-3-540-21459-5",

volume = "2972",

series = "Lecture Notes in Computer Science",

pages = "190--201",

booktitle = "MICAI 2004: Advances in Artificial Intelligence",

note = "Third Mexican International Conference on Artificial Intelligence ; Conference date: 26-04-2004 Through 30-04-2004",

}

Ireland, A, Ellis, WJ & 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, Lecture Notes in Computer Science, vol. 2972, pp. 190-201, Third Mexican International Conference on Artificial Intelligence, Mexico City, Mexico, 26/04/04. https://doi.org/10.1007/978-3-540-24694-7_20

Invariant patterns for program reasoning. / Ireland, Andrew; Ellis, William James; Ingulfsen, Tommy.

MICAI 2004: Advances in Artificial Intelligence: Third Mexican International Conference on Artificial Intelligence, Mexico City, Mexico, April 26-30, 2004. Proceedings. Vol. 2972 2004. p. 190-201 (Lecture Notes in Computer Science; Vol. 2972).

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

TY - CHAP

T1 - Invariant patterns for program reasoning

AU - Ireland, Andrew

AU - Ellis, William James

AU - Ingulfsen, Tommy

PY - 2004

Y1 - 2004

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

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

UR - http://www.scopus.com/inward/record.url?scp=9444232287&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-24694-7_20

DO - 10.1007/978-3-540-24694-7_20

M3 - Chapter (peer-reviewed)

SN - 978-3-540-21459-5

VL - 2972

T3 - Lecture Notes in Computer Science

SP - 190

EP - 201

BT - MICAI 2004: Advances in Artificial Intelligence

T2 - Third Mexican International Conference on Artificial Intelligence

Y2 - 26 April 2004 through 30 April 2004

ER -

Invariant patterns for program reasoning

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this