 |
Home
Call for papers
Program committe
Registration
Conference program
Accomodation
General Information
|
|
|
|
Monday
January 21
- 8.30-9.30: Registration
- 9.30- 10.15: Invited
Talk - Javier Esparza
- 10.15-10.45: Coffee Break
- 10.45-12.45: Session
1 - Security and Protocols
- Combining Abstract
Interpretation and Model Checking for analysing Security Properties
of Java Bytecode
by C. Bernardeschi, and N. De Francesco
- Proofs Methods for
Bisimulation based Information Flow Security
by R. Focardi, C. Piazza , S. Rossi
- A formal correspondence
between offensive and defensive JavaCard virtual machines
by G. Barthe, G. Dufay, L. Jakubiec, S. Melo de Sousa
- Analyzing Cryptographic
Protocols in a Reactive Framework
by RK Shyamasundar
- 12.45-14.00: Lunch
- 14.00-15.30: Session
2 - Timed Systems and Games
- An Abstract Schema
for Equivalence Checking Games
by Li Tan
- Synchronous Closing
of Timed SDL Systems for Model Checking
by Natalia Sidorova and Martin Steffen
- Automata-theoretic
Decision of Timed Games
by Marco Faella, Salvatore La Torre and Murano Aniello.
- 15.30-16.00: Coffee Break
- 16.00-18.00: Session
3 - Static Analysis
- Compositional Termination
Analysis of Symbolic Forward Analysis
by W.Charatonik, S.Moukhopadhyay, and A.Podelski
- Combining Norms to
Prove Termination
by Samir Genaim, Michael Codish, John Gallagher and Vitaly Lagoon
- Static Monotonicity
Analysis for Lambda-definable Functions over Lattices
by Andrzej Murawski and Kwangkeun Yi
- A refinement of the
Escape Property
by Patricia Hill, and Fausto Spoto
- 20.30: Social Dinner
Tuesday
January 22
- 9.00-10.30: Session 4
- Optimization
- Storage Size Reduction
by In-place Mapping of Arrays
by R.Troncon, M.Bruynooghe, G.Jannsens, and F.Catthoor
- Verifying BDD Algorithms
through Monadic Interpretation
by S. Krstic and J. Matthews
- Improving the Encoding
of LTL Model Checking into SAT
by A.Cimatti, M.Pistore, M.Roveri, and R.Sebastiani
- 10.30-11.00: Coffee Break
- 11.00-13.00: Session
5 - Types and Verification
- Automatic Verification
of Probabilistic Free Choice
by A.Pnueli, and L.Zuck
- An experiment in
type inference and verification by abstract interpretation
by Roberta Gori, and Giorgio Levi
- Weak Muller Acceptance
Conditions for Tree Automata
by Salvatore La Torre,
Margherita Napoli and Aniello Murano
- A fully abstract
model for higher-order mobile ambients
by M.Coppo and M. Dezani-Ciancaglini
- 13.00-14.30: Lunch
- 14.30-16.30: Session
6 - Temporal Logics and Systems
- A Simulation Preorder
for Abstraction of Reactive Systems
by F.L.Tiplea, A.Tiplea
- Approximating ATL*
in ATL
by Aidan Harding, Mark Ryan, and Pierre-Yves Schobbens
- Model checking modal
transition systems using Kripke structures
by Michael Huth
- Parameterized Verification
of a Cache Coherence Protocol: Safety and Liveness
by K. Baukus, Y.Lakhnech, and K.Stahl
- 16.30: Conclusions -
End of the Worksop
|
