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.

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. Xavier_Leroy_VPT-2018_abstract.pdf  (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. Bozic_Marsso_Mateescu_Wotawa_paper

    Robert Glück.
    An Experiment in Ping-Pong Protocol Verification by Nondeterministic Pushdown Automata. Glueck_paper

    Hubert Garavel, Lina Marsso.
    Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm. Garavel_Marsso_paper

      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. Kostis_Sagonas_VPT-2018_abstract.pdf  (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. Meunier_Thierry-Mieg_Encrenaz_paper.pdf

    Franco Mazzanti and Alessio Ferrari.
    Ten Diverse Formal Models for a CBTC Automatic Train Supervision System. Mazzanti_Ferrari_paper.pdf

 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. Han_Zhai_Nielsen_Nyman_paper.pdf

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

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