5th International Workshop on Automated Verification of Critical Systems

University of Warwick, UK

All talks will be in Felden Hall, near Arden House, Westwood Campus, University of Warwick. Lunches, as well as Sunday dinner will be at Arden House. Dinner on Monday will be at Scarman House on the main campus.

Monday, 12 September 2005

9.25	Opening
Invited talk
9.30	Cliff Jones Tackling Partial Functions in the Formal Development of Programs
10.30	Coffee break
Contributed talks: Deductive verification
11.00	Mike Gordon, Juliano Iyoda, Scott Owens and Konrad Slind Automatic Formal Synthesis of Hardware from Higher Order Logic
11.30	Hasan Amjad Verification of AMBA Using a Combination of Model Checking and Theorem Proving
12.00	Damian Barsotti, Leonor Prensa Nieto and Alwen Tiu Verification of Clock Synchronization Algorithms: Experiments on a Combination of Deductive Tools
12.30	Lunch
Special session on timed and stochastic systems
2.00	Patricia Bouyer Optimal Timed Games
Contributed talks: Games and concurrent verification
2.45	Dimitar Guelev, Mark Ryan and Pierre Yves Schobbens Synthesising Features by Games
3.15	Tobe Toben and Bernd Westphal Concurrent LSC Verification
3.45	Tea break
Contributed talks: Software verification
4.15	Milan Česka, Pavel Erlebach and Tom Vojnar Pattern-Based Verification of Programs with Extended Linear Linked Data Structures
4.45	Nathaniel Charlton Verification of Java Programs with Interacting Analysis Plugins
Special session on systems biology
5.15	Sara Kalvala Application of Formal Methods to Biological Systems
6.00	Business meeting
7.30	Workshop dinner

Tuesday, 13 September 2005

Invited talk
9.00	James Worrell On Metric Temporal Logic and Faulty Turing Machines
Contributed talks: Timed and hybrid systems
10.00	Eun-Young Kang and Stephan Merz Predicate Diagrams for the Verification of Real-Time Systems
10.30	Hosung Song, Kevin Compton and William Rounds SPHIN: A Model Checker for Reconfigurable Hybrid Systems Based on SPIN
11.00	Coffee break
Contributed talks: Process algebraic verification
11.30	Jane Sinclair, Joy Reed and Bill Roscoe Machine-Verifiable Responsiveness
12.00	Neil Evans and Helen Treharne Linking Semantic Models to Support CSP || B Consistency Checking
12.30	Lunch
Special session on timed and stochastic systems
2.00	Joost-Pieter Katoen Could it Probably be Cheap?
Short presentations
2.45	Aleksandar Dimovski, Dan Ghica and Ranko Lazic Data-Abstraction Refinement for Game Semantics Based Model Checking
3.00	Rajagopal Nagarajan, Nikolaos Papanikolaou, Garry Bowen and Simon Gay An Automated Analysis of the Security of Quantum Key Distribution
3.15	Tea break
3.45	Mike Dodds and Detlef Plump Static Checking of Structural Properties of Heap Data
4.00	Diyaa-Addein Atiya, Nestor Catano and Gerald Luettgen Towards a Benchmark for Model Checkers of Asynchronous Concurrent Systems
4.15	Arun Chakrapani Rao Evaluation of Formal Verification Technology at IARC
4.30	Closing