[lou1306]

(Just for the sake of nitpicking: the term is "liveness")

Short answer is no (seemingly). From the docs it seems Fault only supports assertions. Finding an assertion violation is a reachability problem and is immediately usable to prove safety problems, not liveness.

But, long answer is "kind of"!

That a counterexample to a liveness property ("x eventually happens") generally is a lasso-shaped execution (so a prefix + a cycle) where x never happens. With that in mind, you can reduce liveness checking to reachability: the only problem is, you have to add state-tracking to your model and assert "the system never closes a cycle when x never happens".

This is explained in detail, e.g., in Armin Biere, Cyrille Artho, and Viktor Schuppan. 2002. Liveness Checking as Safety Checking. Electron. Notes Theor. Comput. Sci. 66, 2 (2002), 160–177. DOI:https://doi.org/10.1016/S1571-0661(04)80410-9

[laserbeam]

> (Just for the sake of nitpicking: the term is "liveness")

I appreciate the nitpick, I'm new to this :).