(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
• The SAS 2006 paper can be found in this page and my thesis's page (FR)
• It is written in OCaml above the generic analyser of B. Jeannet now called Fixpoint.
• The tool paper accepted in TAPAS workshop (2010) can be found here(pdf).

Current Version (Linux i386 binary)

• Up-to-date aspicv3.1 binary(March2010). Type aspic --help to display features. Please carefully read the aspic characteristics
• June 2009 : New feature : random actions x'=? are now allowed
• August 2009 : corrected a bug in guard syntax.

Examples

• The (official) benchmark page.
• A disclaimerabout the Aspic results reported by Nicolas Caniart in his CAV 2010 Paper "Merit: an Interpolating Model-Checker".