Laure Gonnord_Research_ASPIC

(logo by Isabelle Borne)

About

• 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).

Examples

• 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".