An experimental framework for temporal verification based on first-order linear-time temporal logic. Our goal is to express transition systems in first-order logic and verify temporal correctness properties, including safety and liveness.
This was an experiment to use the BDD checker's ability to generate the set of all backwards-reachable states to try and come up with an invariant that would hold for any sort sizes. It currently works for lockserver, but the BDD checker is too slow to test it on longer examples. (Also, the current invariant inference part of the implementation can only generate forall invariants.)
This was an experiment to use the BDD checker's ability to generate the set of all backwards-reachable states to try and come up with an invariant that would hold for any sort sizes. It currently works for
lockserver, but the BDD checker is too slow to test it on longer examples. (Also, the current invariant inference part of the implementation can only generateforallinvariants.)