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.


   Friday, April 20



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





    Xavier Leroy (Inria, Paris, France).
    Formal Verification of Code Generators for Modeling Languages. Xavier_Leroy_VPT-2018_abstract.pdf (slides: VPT-MARS-2018-Leroy_presentation.pdf )  (Invited talk)


  Coffee Break


    Cryptographic Protocols

    Josip Bozic, Lina Marsso, Radu Mateescu and Franz Wotawa.
    A Formal TLS Handshake Model in LNT. Bozic_Marsso_Mateescu_Wotawa_paper (slides: MARS-VPT-2018-Bozic_Marsso_Mateescu_Wotawa_presentation.pdf )  (Invited talk)

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

    Hubert Garavel, Lina Marsso.
    Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm. Garavel_Marsso_paper (slides: MARS-VPT-2018-Garavel_Marsso_presentation.pdf )

      MARS and VPT business meetings (everyone welcome)




    Kostis Sagonas (Uppsala University, Sweden).
    Progress on Algorithms for Stateless Model Checking. Kostis_Sagonas_VPT-2018_abstract.pdf  (Invited Tutorial)


    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 (slides: MARS-VPT-2018-Meunier_Thierry-Mieg_Encrenaz_presentation.pdf )

    Franco Mazzanti and Alessio Ferrari.
    Ten Diverse Formal Models for a CBTC Automatic Train Supervision System. Mazzanti_Ferrari_paper.pdf (slides: MARS-VPT-2018-Mazzanti_Ferrari_presentation.pdf )


  Coffee Break


    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 (slides: MARS-VPT-2018-Han_Zhai_Nielsen_Nyman_presentation.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 (slides: VPT-MARS-2018-Beckert_Bingmann_Kiefer_Sanders_Ulbrich_Weigl_presentation.pdf )

John Gallagher,
Alexei Lisitsa,
Andrei P. Nemytykh,