ASPIC "Manual" . Laure Gonnord

Aspic aims at generating invariants from a (variant of) FAST files : 
-- the comments are only of the form // . comments of the form /**/
will lead to a syntax error.
-- The initial region has keyword "init", for instance : 
     region init := {state = s1 && x=0};
-- The optional bad region has keyword bad :
     region bad := ...
-- for the moment aspic does not support the usage of non convex
regions : || (or) and ! (not) are not allowed in the region
definitions

Aspic options : ./aspic --help

Remarks : 
--Aspic does not deal with integers, so it won't prove any
formula that relies on arithmetic properties.
-- Aspic is designed to generate numerical invariants with the use of
the polyhedral abstract domains. Aspic is not good at proving
invariants that relies on tricky use of booleans encoded as integers
(such as protocols).
-- Aspic is only able to prove SAFETY properties. Use other provers if
you want to prove the non-reachability of a region.


---------------------------------------------------
Aspic 2005/2016 by Laure Gonnord
Aspic homepage : http://laure.gonnord.org/pro/aspic
Please report bugs : aspic@gonnord.org