Third International Workshop on
Verification, Model Checking and Abstract Interpretation


Call for papers

Program committe


Conference program


General Information









Monday 21 | Tuesday 22

Preliminary Program

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