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