09:30-10:30: Andrew Ireland:
Cooperative Reasoning for Automatic Software Verification
10:30-11:00: Coffee Break
11:00-11:05: Natasha Alechina, Brian Logan, Nguyen Hoang Nga and Adbur Rakib:
Verification of resource-bounded multi-agent systems
11:05-11:10: Abdelkader Behdanna, Clare Dixon and Michael Fisher:
Analyzing the Behaviour of a Swarm of Foraging Robots Using Temporal Specification and Verification
11:10-11:15: Alessandro Basso, Alexander Bolotov and Vladimir Getov:
Automata-based Formal Specification of Stateful Systems
11:15-11:20: Louise A. Dennis, Rafael H. Bordini, Berndt Farwer and Michael Fisher:
Model-Checking Agent Programming Languages
11:20-11:25: Holger Gast:
Towards Verification by Symbolic Degugging
11:25-11:30: Andrew Ireland, Ewen Maclean and Ianthe Hind:
Proving Functional Properties in Separation Logic
11:30-12:30: Session 3: Poster Session
12:30-14:00: Lunch
14:00-15:30: It is impossible to automatically generate good representations for reasoning problems?
15:30-16:00: Coffee Break
16:00-16:05: James P. Bridge, Lawrence C. Paulson and Sean B. Holden:
Applying Machine Learning to Heuristic Selection in an Automatic Theorem Prover
16:05-16:10: Lucas Dixon and Dominic Mulligan:
Dynamic Relational Rippling for HOL
16:10-16:15: Andrew Priddle-Higson, Alan Bundy, Fiona McNeill and Burkhard Schafer:
Ontology Evolution in Law
16:15-16:20: Alan P. Sexton and Volker Sorge:
Reasoning on Abstract Matrix Structures
16:20-16:25: Pedro Torres and Simon Colton:
Toward Meta-Level Theory Formation
16:25-16:30: Lan Zhang, Ullrich Hustadt and Claire Dixon:
A Refined Resolution Calculus for CTL
16:30-17:30: Session 6: Poster Session
09:30-10:30: Steve Linton:
Symmetry and Search -- A Survey
10:30-11:00: Coffee Break
11:00-11:05: Alexander Bolotov:
Tackling 'Until Induction' in Natural Deduction for PLTL
11:05-11:10: Clare Dixon and John C. McCabe-Danste:
Resolution-Based Proof for a Temporal Logic of Robustness
11:10-11:15: Manfred Kerber:
Normalizations in Propositional Logic
11:15-11:20: Michel Ludwig and Ullrich Hudstadt:
Fair Monodic Temporal Logic Proving
11:20-11:25: Hilver Reker:
A Heuristic for Tableau Reasoning Based on Tree Decompositions of Knowledge Bases
11:25-11:30: Robert Rothenberg:
On the Correspondance between Hypersequent and Labelled Calculi for Intermediate Logics
11:30-12:30: Session 9: Poster Session
12:30-14:00: Lunch
14:00-15:30: What should make successful research in automated reasoning?
15:30-16:00: Coffee Break
16:00-17:00: ARW Committee Meeting