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.

• The EiffelStudio compiler.
• The Boogie program verifier.

Download gin-pink

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

• Version 0.03 (released 4 September 2009, compiled with EiffelStudio 6.3)
  • Source and pre-compiled Windows and GNU/Linux versions: download (tarball, 1.3 Mb)
  • Experiments from the paper: "Inferring Loop Invariants using Postconditions": download (tarball, 76 Kb)