Ninth International Workshop on
Verification and Program Transformation

The Ninth International Workshop on Verification and Program Transformation (VPT-2021) aims to bring together researchers working in two different areas, Verification and Program Transformation.

VPT-2021 will be an ETAPS-2021 Workshop, and held online on March 27th and 28th, 2021, Luxembourg, Luxembourg.

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

The VPT 2021 event will consist of two parts:


Online registration desk:

Please, note that Europe will switch to daylight saving time during the night between Sat 27 March and Sun 28.

   Saturday, March 27





  Sessions 1, 2.

   Chairs: Alexei P. Lisitsa and Andrei P. Nemytykh


    Professor Alberto Pettorossi (Università di Roma Tor Vergata, Italy). A Historical Account of my Early Research Interests.   Alberto_Pettorossi_VPT-2020_abstract.pdf (EPTCS, Vol. 320, pp. 128 EPTCS, Vol. 320, pp. 128 slides: Alberto-Pettorossi-VPT-2021-Luxembourg.pptx ) (Keynote speech)


  Coffee Break


    Maurizio Proietti (IASI-CNR, Rome, Italy) From Program Transformation to Program Verification.
    (Joint work with Emanuele De Angelis, Fabio Fioravanti)   Maurizio_Proietti_VPT-2020_abstract.pdf (EPTCS, Vol. 320, pp. 95109 EPTCS, Vol. 320, pp. 95109 , slides: VPT-20-21-Maurizio_Proietti_presentation.pdf ) (Invited talk)


    Lorenzo Clemente (University of Warsaw, Department of Mathematics, Informatics and Mechanic, Poland).
    On the complexity of the universality and inclusion problems for unambiguous context-free grammars.   Lorenzo_Clemente_VPT-2020_abstract.pdf (EPTCS, Vol. 320, pp. 2943 EPTCS, Vol. 320, pp. 2943 , slides: VPT-20-21-Lorenzo_Clemente_presentation.pdf ) (Invited talk)



  Session 3.

   Chair: Maurizio Proietti


    John P. Gallagher (Roskilde University, Denmark and IMDEA Software Institute, Spain). From Big-Step to Small-Step Semantics and Back with Interpreter Specialisation.
    (Joint work with Hermenegildo, Kafle, Klemen, López García and Morales)   John_Gallagher_VPT-2020_abstract.pdf (EPTCS, Vol. 320, pp. 5064 EPTCS, Vol. 320, pp. 5064 , slides: VPT-20-21-John_P_Gallagher_presentation.pdf ) (Invited talk)


    Horatiu Cirstea, Alexis Grall, Dominique Méry. Generating Distributed Programs from Event-B Models. (EPTCS, Vol. 320, pp. 110124 EPTCS, Vol. 320, pp. 110124 , slides: VPT-20-21-Horatiu_Cirstea-Alexis_Grall-Dominique_Mery_presentation.pdf )


  Coffee Break

  Session 4.

   Chair: Fritz Henglein


    Neil D. Jones (Professor emeritus at University of Copenhagen, Denmark) Cons-free Programs and Complexity Classes between L and P.
    (Joint work with Siddharth Bhaskar, Cynthia Kop, Jakob Simonsen)   Neil_Jones_VPT-2020_abstract.pdf (EPTCS, Vol. 320, pp. 6579 EPTCS, Vol. 320, pp. 6579 , slides: VPT-20-21-Siddharth_Bhaskar-Neil_D_Jones-Cynthia_Kop-Jakob_Simonsen_presentation.pdf ) (Invited talk)


    Dimitur Nikolaev Krustev. Optimizing Program Size Using Multi-result Supercompilation. (EPTCS, Vol. 320, pp. 125139 EPTCS, Vol. 320, pp. 125139 , slides: VPT-20-21-Dimitur_Krustev_presentation.pdf )


  Coffee Break

  Session 5.

   Chair: John P. Gallagher


    Moa Johansson (Chalmers University, Gothenburg, Sweden) Theory Exploration: Conjecturing, Testing and Reasoning about Programs. Moa_Johansson_VPT-2020_abstract.pdf ( slides: VPT-20-21-Moa_Johansson_presentation.pdf )  (Invited talk)


    Geoff W. Hamilton. Distilling Programs to Prove Termination. (EPTCS, Vol. 320, pp. 140154 EPTCS, Vol. 320, pp. 140154 , slides: VPT-20-21-Geoff_W_Hamilton_presentation.pdf )


  Coffee Break


    Michael Leuschel (Heinrich-Heine-Universität Düsseldorf, Germany) Prolog for Verification, Analysis and Transformation Tools.   Michael_Leuschel_VPT-2020_abstract.pdf
    (EPTCS, Vol. 320, pp. 8094 EPTCS, Vol. 320, pp. 8094 , slides: VPT-20-21-Michael_Leuschel_presentation.pdf ) (Invited talk)

Please, note that Europe will switch to daylight saving time during the night between Sat 27 March and Sun 28.

   Sunday, March 28
  Session 1.

   Chair: Geoff W. Hamilton


    Michael Norrish (Australian National University, Australia). CakeML: Verified Computation/Compilation Stories.   Michael_Norrish_VPT-2020_abstract.pdf ( slides: VPT-20-21-Michael_Norrish_presentation.pdf )   (Invited talk)


    Isabella Mastroeni, Vincenzo Arceri. Improving Dynamic Code Analysis by Code Abstraction. (preprint VPT2021_paper_4.pdf , slides: VPT-20-21-Isabella-Mastroeni_Vincenzo-Arceri_presentation.pdf )


  Coffee Break

  Session 2.

   Chair: Laura Kovacs


    Agostino Cortesi (Università Ca' Foscari, Venezia, Italy).
    Abstract Interpretation and Program Transformation: techniques running after each other.   Agostino_Cortesi_VPT-2021_abstract.pdf (slides: VPT-20-21-Agostino_Cortesi_presentation.pdf )   (Invited talk)


    Maria Bendix Mikkelsen, Robert Glück, Maja H. Kirkeby. An Inversion Tool for Conditional Term Rewriting Systems. (extended abstract VPT2021_paper_2.pdf , slides: VPT-20-21-Maria_Bendix_Mikkelsen-Robert_Glueck-Maja_H_Kirkeby_presentation.pdf )



  Session 3.

   Chair: Alberto Pettorossi


    Nikos Gorogiannis (Facebook London, UK). A Compositional Deadlock Analysis for Code Commits in Android Java.   Nikos_Gorogiannis_VPT-2021_abstract.pdf (Invited talk)


    Antonina Nepeivoda. Program Specialization as a Tool for Solving Word Equations.   (preprint VPT2021_paper_1.pdf , slides: VPT-20-21-Antonina_Nepeivoda_presentation.pdf )


  Coffee Break

  Session 4.

   Chairs: Alexei P. Lisitsa and Andrei P. Nemytykh


    Fritz Henglein (University of Copenhagen and Deon Digital, Denmark). Verified Abstract Interpretation of Digital Contracts.   Fritz_Henglein_VPT-2021_abstract.pdf (slides: VPT-20-21-Fritz_Henglein_presentation.pdf )   (Invited talk)


    Ekaterina Verbitskaia, Daniil Berezun, Dmitry Boulytchev. An Empirical Study of Partial Deduction for MiniKanren.   (preprint VPT2021_paper_3.pdf , slides: VPT-20-21-Ekaterina_Verbitskaia-Daniil_Berezun-Dmitry-Boulytchev_presentation.pdf )


  Coffee Break

  Session 5.

   Chair: Lorenzo Clemente


    Benjamin Kaminski (University College London, UK). Latticed k-Induction with an Application to Probabilistic Programs.   Benjamin_Kaminski_VPT-2021_abstract.pdf (Invited talk)


    Laura Kovacs (Vienna University of Technology, Austria). Trace Logic for Automating Loop Reasoning.   Laura_Kovacs_VPT-2021_abstract.pdf ( slides: VPT-20-21-Laura_Kovacs_presentation.pdf )  (Invited talk)


  Coffee Break

  Reminiscences session


    Sophie Renault (European Patent Office – The Hague, The Netherlands). Transforming programs with Alberto in the Rome of the last century   Sophie_Renault_VPT-2020_abstract.pdf (Invited talk)


    Andrzej Skowron (Professor emeritus at University of Warsaw, Poland). Alberto Pettorossi, the great scientist and my dear friend   Andrzej_Skowron_abstract.pdf (Invited talk)


      Welcome to talk



Alexei Lisitsa,
Andrei P. Nemytykh,