Could We Have Chosen a Better Loop Invariant or Method Contract?

The method contract and loop invariant rules (contract rules) are an important software verification technique for handling method invocations and loops. However, if a verification condition resulting from using a contract rule turns out to be falsifiable, then the user does not know if she could have chosen a stronger contract to verify the program or if the program is not verifiable due to a software bug. We approach this problem and present a novel technique that unifies verification and software bug detection.

• Type: Conference
• Year: 2009
• Where: TAP
• Authors: Christoph Gladisch
• Keywords: Contract Rule, Hardware, Method Contract, Software Verification Technique, TAP 2009