Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 ARMC-Live: Software Model Checker for Liveness Properties
ARMC-Live: Software Model Checker for Liveness Properties
ARMC-Live is a model checker for verification of liveness
properties of infinite-state systems via transition invariants. It
computes an inductive transition invariant of a given program and
tests if the computed transition invariant is strong enough to prove
the given property, given as an LTL formula.
The tool is written in SICStus Prolog. We use LTL2BA
translator to convert an LTL formula expressing fairness assumptions
and the property into a Büchi automaton.