Invariant Patterns for Program Reasoning

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.

• Type: Conference
• Year: 2004
• Where: MICAI
• Authors: Andrew Ireland, Bill J. Ellis, Tommy Ingulfsen
• Keywords: Artificial Intelligence, Automatic Invariant Generation, Invariant Patterns, Invariant Schemas, MICAI 2004