Joint work with E. Clarke, S. Jha, B. Krogh
Counterexample guided abstraction refinement, a powerful technique for
verifying properties of discrete-state systems has been extended recently
to hybrid systems verification. However, unlike in discrete systems,
establishing the successor relation for hybrid systems can be a fairly
expensive step since it requires evaluation and overapproximation
of the continuous dynamics. It has been observed that it is often
sufficient to consider fragments of counterexamples rather than complete
counterexamples.
This talk presents a generalization of the idea of fragments. We extend the notion of cut sets in network flows to cutting sets of fragments in abstractions. Cutting sets of fragments are then used to guide the abstraction refinement in order to prove safety properties for hybrid systems.
| Ansgar Fehnker |
| Recently joined researcher in the NICTA Formal Methods program |
| Date: | Thu Dec 2 2004 |
| Time: | 1 to 2pm |
| Location: | Level 1 Seminar Room, CSE Bldg (K17), UNSW Kensington campus |
Last updated by tbourke at Fri Nov 26 19:01:13 2004 GMT+1100