Invariants about the future
Eric Koskinen ( Cambridge University )
- 11:00 20th May 2010 ( week 4, Trinity Term 2010 )Room 051, Oxford University Computing Laboratory
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.