Workshop Programme: Verification and Computational Logic

Prelimnary Programme for the

Note: a buffer time of 5-10 minutes per talk is added at the end of each session.

14:30 WELCOME
14:35 - 15:25 Invited Talk 1
"Data independent induction"
Bill Roscoe
15:25 - 15:55 Talk 1
"Verification of Communicating Processes in the Event of Interface Difference"
Jonatha Burton, Maciej Koutny
16:05 - 16:30 Coffee Break
16:30 - 17:20 Invited Talk 2
"Infinite State Model Checking with Tableaux"
Julian Bradfield
17:20 - 17:50 Talk 2
"Fair Model Checking of Abstractions"
Dennis Dams, Rob Gerth, Orna Grumberg

9:00 - 9:50 Invited Talk 3
Faron Moller
10:00 - 10:30 Morning Coffee
10:30 - 11:00 Talk 3
"Verification of Petri net properties in CLP"
Guy A. Narboni
11:00 - 11:30 Talk 4
"On-the-fly optimized model checking under the symbolic approch"
Khalil Ajami
11:40 - 11:50 Short Break
11:50 - 12:20 Talk 5
"A Rewriting Prolog Semantics"
M. Kulas
12:20 - 12:50 Talk 6
"Well-Typed Programs are not Wrong"
Pierre Derensart, Jan-Georg Smaus
13:00 - 14:30 Lunch
14:30 - 15:20 Invited Talk 4 "Analysing broadcast protocols by infinite state model checking"
Javier Esparza
15:20 - 15:50 Talk 7
"A Finite Covering Tree for Analysing Entropic Broadcast Protocols"
Alain Finkel, Jerome Leroux
16:00 - 16:30 Coffee Break
16:30 - 17:00 Talk 8
"Weakly Continuation-Closed Abstraction can be Defined on Trace Reductions"
Ulrich Ultes-Nitsche, Simon St-James
17:00 - 17:30 Talk 9
"LTL Model Checking of CSP by Refinement"
Andrew Currie, Michael Leuschel, Thierry Massart
17:40 CLOSING