(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)


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