(logo by Isabelle Borne)
- This software is based on Linear Relation Analysis, and combines classic LRA (with widening) and acceleration techniques.
- It has nothing to do with rugby nor paragliding
- Theoretical fundations : the SAS06 paper, the SCP journal paper (with P. Schrammel) and tool paper.
- It is written in OCaml above the generic analyser of B. Jeannet now called Fixpoint.
- The Aspic input format can be generated using C2fsm, a C-frontend written by Paul Feautrier. The two tools are part of the WTC toolsuite for proving termination of sequential programs : demo .
Current Version (Linux i386 binary)
- aspicv3.4 binary(Jan 2015, i386/64bits). Better log printing.
- aspicv3.3 binary(Nov2013). Type aspic --help to display features. Please carefully read the aspic characteristics
- (2012/02/07) Aspic grammar and Aspic Ocaml parser (Aspic input language is a minor modification of the FastER input format).
- The (official) benchmark page.
- These examples are also part of the Alice benchmarck, maintained by V. Maisonneuve.
- A disclaimer about the Aspic results reported by Nicolas Caniart in his CAV 2010 Paper "Merit: an Interpolating Model-Checker".