Loop Invariants from Postconditions

What is gin-pink

gin-pink is a command-line tool that infers loop invariants in annotated Boogie procedures. Invariants are found by first generating mutations of the postcondition and then by checking these candidates against the definition of loop invariant. The technique and the gin-pink tool are presented in the paper "Inferring Loop Invariants using Postconditions".

gin-pink can be used with any high-level language for which a mapping to Boogie is available.

Pre-requisites for usage

gin-pink calls Boogie to verify the candidate invariants, hence Boogie must be installed on your system to exploit this feature. You can still use the candidate generation feature of gin-pink without installing Boogie, though.

You will need the following software to compile and run gin-pink.

Download gin-pink

gin-pink is coded in Eiffel and available both in source and compiled versions under the GPL license.

Valid XHTML 1.0 Strict