|
Conference Programme
|
|
Tutorial Programme (20-21/11/2006) |
Wednesday 22/11/2006 |
Thursday 23/11/2006 |
Friday 24/11/2006
|
|
Keynote Speakers |
List of Accepted Papers
|
|
|
Day 1: Wednesday, 22 November 2006
|
|
|
08:00
|
REGISTRATION
|
|
|
09:00-09:30
|
OPENING SESSION
|
|
|
09:30-10:30
|
KEYNOTE SPEAKER:
Tobias Nipkow
(Chair: Ali Mili)
|
|
|
Verifying a Hotel Key Card System
|
|
|
by Tobias Nipkow
|
|
|
10:30-11:00
|
COFFEE BREAK
|
|
|
11:00-12:30
|
SESSION 1:
SEMANTICS
(Chair: Ana Cavalcanti)
|
|
|
|
|
|
Quantitative mu-calculus analysis of power management in wireless networks
|
|
|
by Annabelle McIver
|
|
|
|
|
|
Termination and Divergence are undecidable under a Maximum Progress
Multi-Step Semantics for LinCa
|
|
|
by Mila Majster-Cederbaum and Christoph Minnameier
|
|
|
|
|
|
A Topological Approach of the Web Classification
|
|
|
by Gabriel Ciobanu and Danut Rusu
|
|
|
12:30-14:30
|
LUNCH
|
|
|
14:30-16:30
|
SESSION 2:
CONCURRENCY
(Chair: Kamel Barkaoui)
|
|
|
|
|
|
Bisimulation Congruences in the Calculus of Looping Sequences
|
|
|
by Roberto Barbuti, Andrea Maggiolo-Schettini, Paolo Milazzo and Angelo Troina
|
|
|
|
|
|
Stronger Reduction Criteria for Local First Search
|
|
|
by Marcos Kurban, Peter Niebert, HongYang Qu and Walter Vogler
|
|
|
|
|
|
A Lattice-Theoretic Model for an Algebra of Communicating Sequential Processes
|
|
|
by Malcolm Tyrrell, Joseph M. Morris, Andrew Butterfield and Arthur Hughes
|
|
|
|
|
|
A Petri Net Translation of pi-calculus Terms
|
|
|
by Raymond Devillers, Hanna Klaudel and Maciej Koutny
|
|
|
16:30-17:00
|
COFFEE BREAK
|
|
|
17:00-18:00
|
KEYNOTE SPEAKER:
Mike Reed
(Chair: Zhiming Liu)
|
|
MOVED TO
|
Topological Domains for Theoretical Computer Science
|
|
FRIDAY AT 9:00
|
by Mike Reed
|
|
|
19:00
|
RECEPTION
|
|
|
Day 2: Thursday, 23 November 2006
|
|
|
09:00-10:00
|
KEYNOTE SPEAKER:
Jim Woodcock
(Chair: Rahma Ben Ayed)
|
|
|
Z/Eves and the Mondex smart card: a pilot project for the
Grand Challenge in Verified Software
|
|
|
by Jim Woodcock and Leonardo Freitas
|
|
|
10:00-10:30< /strong>
|
COFFEE BREAK
|
|
|
10:30-12:00
|
SESSION 3:
MODEL-CHECKING
(Chair: Antonio Cerone)
|
|
|
|
|
|
Handling Algebraic Properties in Automatic Analysis of Security Protocols
|
|
|
by Yohan Boichut, Pierre-Cyrille Héam and Olga Kouchnarenko
|
|
|
|
|
|
Compositional Algorithm for Parallel Model Checking Polygonal Hybrid Systems
|
|
|
by Gordon Pace and Gerardo Schneider
|
|
|
|
|
|
Thread-Modular Verification is Cartesian Abstract Interpretation
|
|
|
by Alexander Malkis, Andreas Podelski, Andrey Rybalchenko
|
|
|
12:00
|
LUNCH
|
|
|
13:30
|
EXCURSION
|
|
|
20:00
|
BANQUET
|
|
|
Day 3: Friday, 24 November 2006
|
|
|
09:00-10:00
|
KEYNOTE SPEAKER:
Mike Reed
(Chair: Zhiming Liu)
|
|
|
Topological Domains for Theoretical Computer Science
|
|
|
by Mike Reed
|
Zohar Manna's invited talk entitled
Verification Constraint Problems with Strengthening
has been cancelled
|
|
|
10:00-10:30
|
COFFEE BREAK
|
|
|
10:30-12:00
|
SESSION 4:
FORMAL LANGUAGES
(Chair: Yahya Slimani)
|
|
|
|
|
|
Capture-avoiding substitution as a nominal algebra
|
|
|
by Murdoch J. Gabbay and Aad Mathijssen
|
|
|
|
|
|
Prime Decomposition Problem for Several Kinds of Regular Codes
|
|
|
by Kieu Van Hung and Do Long Van
|
|
|
|
|
|
A New Approach to Determinisation Using Bit-Parallelism
|
|
|
by Jan Supol and Borivoj Melichar
|
|
|
12:00-14:00
|
LUNCH
|
|
|
14:00-16:00
|
SESSION 5:
LOGIC AND TYPE THEORY
(Chair: Khaled Bsaies)
|
|
|
|
|
|
Proving ATL* Properties of Infinite-State Systems
|
|
|
by Matteo Slanina, Henny B. Sipma and Zohar Manna
|
|
|
|
|
|
Type safety for FJ and FGJ
|
|
|
by Wang Shuling, Quan Long and Qiu Zongyan
|
|
|
|
|
|
Partizan Games in Isabelle/HOL
|
|
|
by Steven Obua
|
|
|
|
|
|
Proof-producing program analysis
|
|
|
by Chaieb Amine
|
|
|
16:00-16:30
|
COFFEE BREAK
|
|
|
16:30-18:30
|
SESSION 6:
REAL-TIME AND MOBILITY
(Chair: Karim Djouani)
|
|
|
|
|
|
Reachability Analysis of Mobile Ambients in Fragments of AC Term Rewriting
|
|
|
by Giorgio Delzanno and Roberto Montagna
|
|
|
|
|
|
Interesting Properties of the Real-Time Conformance Relation tioco
|
|
|
by Moez Krichen and Stavros Tripakis
|
|
|
|
|
|
Model Checking Duration Calculus: A Practical Approach
|
|
|
by Roland Meyer, Johannes Faber, Andrey Rybalchenko
|
|
|
|
|
|
Spatio-Temporal Model Checking for Mobile Real-Time Systems
|
|
|
by Jan-David Quesel and Andreas Schaefer
|
|
|
18:30-18:45
|
CLOSING SESSION
|
|