Static IMPerative AnaLyzer
Java GAP
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.


SIMPAL (Static IMPerative AnaLyzer) is a tool built to perform compositional reasoning of imperative programs.

It features a domain specific language called Limp (a portmanteau of Lustre imperative). These programs are then compiled into a control flow graph (CFG) and translated into a Lustre model, which can then be analzyed.

The analysis is performed by JKind, which is embedded into the tool directly, thus it is not necessary to install it.

The tool does require the user to install:

A document describing the function and features of the tool and the Limp language is available in the source repository at:

keywords: compositional reasoning imperative viability reachability jkind k-induction lustre control flow