11-13th September 2013

Guildford, Surrey

13th International Workshop on Automated Verification of Critical Systems

Workshop Programme

Wednesday
11:00-12:00 Registration outside LTM (Lecture Theatre M)
12:00-13:50 Lunch (informal buffet outside LTM)
13:50-14:00 Welcome
14:00-15:30 Session chair: Jaco van de Pol

  • Bogdan Tofan, Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler and Wolfgang Reif
    Compositional Verification of a Lock-Free Stack with RGITL
  • Vahid Hashemi, Holger Hermanns and Andrea Turrini
    On the Efficiency of Deciding Probabilistic Automata Weak Bisimulation
  • Brijesh Dongol and John Derrick
    Simplifying proofs of linearisability using layers of abstraction
15:30-16:00 Coffee Break (outside LTM)
16:00-16:30 Session chair: Helen Treharne

  • Zeinab Sharifi, Mahdi Mosaffa, Siamak Mohammadi and Marjan Sirjani
    Functional and Performance Analysis of Network-on-Chips Using Actor-based Modeling and Formal Verification
16:30-17:00 Session chair: Helen Treharne

Invited Talk: Sofia Guerra, Adelard
Keeping the temperature down: assessing smart instruments for the nuclear industry
17:15-17:45 PC meeting (TBC)
Evening Own arrangements - e.g., eating in Guildford informally together

Thursday
9:00-10:00 Session chair: Markus Roggenbach

Invited Talk: Alessio Lomuscio
Verification of multi-agent systems via model-checking
10:00-10:10 Group photo (outside, amphitheatre outside the lecture theatre block)
10:10-10:30 Coffee Break (outside LTM)
10:30-12:00 Session chair: Brijesh Dongol

  • Gerald Lüttgen and Walter Vogler
    Richer Interface Automata with Optimistic and Pessimistic Compatibility
  • Dana Dghaym, Michael Butler and Asieh Salehi Fathabadi
    Evaluation of Control Flow Management Approaches for Event-B Modelling
  • Eman Alkhammash, Asieh Salehi Fathabadi, Michael Butler and Corina Cirstea
    Building Traceable Event-B Models from Requirements
12:00-14:00 Lunch (in Lakeside restaurant on campus)
13:55-14:00
Jaco van de Pol
Introduction to AVOCS 2014
14:00-15:30 Session chair: Gerald Lüttgen

  • Alexandre David, Kim Guldstrand Larsen, Axel Legay and Danny Bøgsted Poulsen
    Statistical Model Checking of Dynamic Networks of Stochastic Hybrid Automata
  • Georges Morbé and Christoph Scholl
    Fully Symbolic TCTL Model Checking for Incomplete Timed Systems
  • Marcello M. Bersani, Matteo Rossi and Pierluigi San Pietro
15:30-16:00 Coffee Break (outside LTM)
16:00-17:00 Session chair: Michael Goldsmith

  • Murat Moran and James Heather
    Automated Analysis of Voting Systems with Dolev-Yao Intruder Model
  • Efstathios Stathakidis, David M. Williams and James Heather
    Verifying a Mix Net in CSP
19:00- Conference Dinner in a local restaurant in Guildford

Friday
9:00-10:00 Session chair: Steve Schneider

Invited Talk: Marco Roveri
Software Model Checking With Explicit Scheduler and Symbolic Threads
10:00-10:30 Coffee Break (outside LTM)
10:30-12:00 Session chair: David Williams

  • Alexander Knapp, Liam O'Reilly, Markus Roggenbach and Holger Schlingloff
  • Tomohiro Kaizu, Yoshinao Isobe and Masato Suzuki
    Verifying sequence diagrams using the process algebra CSP
    (shortpaper)
  • Zamira Daw, Rance Cleaveland and Marcus Vetter
    Integrating of model checking and UML based model-driven development for embedded systems
  • Lucian Patcas, Mark Lawford and Tom Maibaum
    From System Requirements to Software Requirements in the Four-Variable Model
12:00-12:10 Closing
12:10-14:00 Lunch - in Hillside & Farewell