Workshop Program

MARS / VPT 2018

Friday 20 April 2018, Aristotelis II

08:00 Registration opens
08:45 Welcome
09:00 – 10:00 Invited Presentation
Formal Verification of Code Generators for Modeling Languages
Xavier Leroy
10:00 – 10:30 Coffee Break
10:30 – 12:00 Cryptographic protocols
A Formal TLS Handshake Model in LNT
Josip Bozic, Lina Marsso, Radu Mateescu and Franz Wotawa
An Experiment in Ping-Pong Protocol Verification by Nondeterministic Pushdown Automata
Robert Glück
Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm
Hubert Garavel, Lina Marsso
12:00 – 12:30 MARS and VPT business meetings (everyone welcome)
12:30 – 14:00 Lunch Break
14:00 – 15:00 Tutorial
Progress on Algorithms for Stateless Model Checking
Kostis Sagonas
15:00 – 16:00 Comparing different models of the same system
Modeling a Cache Coherence Protocol with the Guarded Action Language
Quentin L. Meunier, Yann Thierry-Mieg and Emmanuelle Encrenaz
Ten Diverse Formal Models for a CBTC Automatic Train Supervision System
Franco Mazzanti and Alessio Ferrari
16:00 – 16:30 Coffee Break
16:30 – 17:30 Modelling avionics and program equivalence
A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems
Pujie Han, Zhengjun Zhai, Brian Nielsen and Ulrik Nyman
Proving Equivalence Between Imperative and MapReduce Implementations Using Program Transformations
Bernhard Beckert, Timo Bingmann, Moritz Kiefer, Peter Sanders, Mattias Ulbrich and Alexander Weigl