Skip to main content

Invariants about the future

Eric Koskinen ( Cambridge University )
In this talk I will introduce a novel symbolic model checking tool for the verification of branching-time properties of infinite-state programs which uses a TERMINATOR-like reduction to a safety problem together with the search for a set of ranking functions.

Share this: