VPT 2018 / Program

Programme
Sixth International Workshop on
Verification and Program Transformation

The Sixth International Workshop on Verification and Program Transformation (VPT-2018) aims to bring together researchers working in two different areas, Verification and Program Transformation. VPT 2018 will be co-located with MARS 2018, MARS/VPT 2018 is an ETAPS 2018 Workshop, and held on April 20th, 2018, Thessaloniki, Greece.

The workshop will provide a forum where all interactions of the two fields can be presented and discussed.

A number of pictures from the workshop:

The MARS/VPT-2018 Proceedings has been published as Volume 268 of Electronic Proceedings in Theoretical Computer Science.

Programme

Friday, April 20

8:00-8:45

Registration

Aristotle University of Thessaloniki (host-institution)
Makedonia Palace, Thessaloniki (venue) / Room: Aristotelis II

ΜΟΥΣΑΙΣ ΧΑΡΙΣΙ ΘΥΕ

8:45-9:00

  Welcome

9:00-10:00

Xavier Leroy (Inria, Paris, France).
Formal Verification of Code Generators for Modeling Languages. (slides: ) (Invited talk)

10:00-10:30

  Coffee Break

10:30-12:00

Cryptographic Protocols

Josip Bozic, Lina Marsso, Radu Mateescu and Franz Wotawa.
A Formal TLS Handshake Model in LNT. (slides: ) (Invited talk)

Robert Glück.
An Experiment in Ping-Pong Protocol Verification by Nondeterministic Pushdown Automata. (slides available from the author )

Hubert Garavel, Lina Marsso.
Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm. (slides: )

  MARS and VPT business meetings (everyone welcome)

12:30-14:00

  Lunch

14:00-15:00

Kostis Sagonas (Uppsala University, Sweden).
Progress on Algorithms for Stateless Model Checking. (Invited Tutorial)

15:00-16:00

Comparing Different Models of the Same System

Quentin L. Meunier, Yann Thierry-Mieg and Emmanuelle Encrenaz.
Modeling a Cache Coherence Protocol with the Guarded Action Language. (slides: )

Franco Mazzanti and Alessio Ferrari.
Ten Diverse Formal Models for a CBTC Automatic Train Supervision System. (slides: )

16:00-16:30

  Coffee Break

16:30-17:30

Modelling Avionics and Program Equivalence

Pujie Han, Zhengjun Zhai, Brian Nielsen and Ulrik Nyman.
A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems. (slides: )

Bernhard Beckert, Timo Bingmann, Moritz Kiefer, Peter Sanders, Mattias Ulbrich and Alexander Weigl.
Proving Equivalence Between Imperative and MapReduce Implementations Using Program Transformations. (slides: )

Contacts
Email:
John Gallagher, jpg@ruc.dk
Alexei Lisitsa, a.lisitsa@csc.liv.ac.uk
Andrei P. Nemytykh, nemytykh@math.botik.ru
Web: http://refal.botik.ru/vpt/vpt2018/
          http://www.etaps.org/index.php/2018/workshops#marsvpt2018

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