Programme
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:

Programme

Online registration desk: https://etaps.org/2021/registration


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

   Saturday, March 27

 08:40-08:55

  Registration

 08:55-09:00

  Welcome

  Sessions 1, 2.

   Chairs: Alexei P. Lisitsa and Andrei P. Nemytykh

 09:00-10:00

    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. 1–28 EPTCS, Vol. 320, pp. 1–28 slides: Alberto-Pettorossi-VPT-2021-Luxembourg.pptx ) (Keynote speech)

 10:00-10:15

  Coffee Break

 10:15-11:00

    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. 95–109 EPTCS, Vol. 320, pp. 95–109 , slides: VPT-20-21-Maurizio_Proietti_presentation.pdf ) (Invited talk)

 11:00-11:45

    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. 29–43 EPTCS, Vol. 320, pp. 29–43 , slides: VPT-20-21-Lorenzo_Clemente_presentation.pdf ) (Invited talk)

 11:45-12:45

  Lunch
  Session 3.

   Chair: Maurizio Proietti

 12:45-13:30

    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. 50–64 EPTCS, Vol. 320, pp. 50–64 , slides: VPT-20-21-John_P_Gallagher_presentation.pdf ) (Invited talk)

 13:30-14:00

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

 14:00-14:15

  Coffee Break
  Session 4.

   Chair: Fritz Henglein

 14:15-15:00

    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. 65–79 EPTCS, Vol. 320, pp. 65–79 , slides: VPT-20-21-Siddharth_Bhaskar-Neil_D_Jones-Cynthia_Kop-Jakob_Simonsen_presentation.pdf ) (Invited talk)

 15:00-15:30

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

 15:30-15:45

  Coffee Break
  Session 5.

   Chair: John P. Gallagher

 15:45-16:30

    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)

 16:30-17:00

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

 17:00-17:15

  Coffee Break

 17:15-18:00

    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. 80–94 EPTCS, Vol. 320, pp. 80–94 , 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

 09:00-09:45

    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)

 09:45-10:15

    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 )

 10:15-10:30

  Coffee Break
  Session 2.

   Chair: Laura Kovacs

 10:30-11:15

    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)

 11:15-11:35

    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 )

 11:35-12:35

  Lunch
  Session 3.

   Chair: Alberto Pettorossi

 12:35-13:20

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

 13:20-13:50

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

 13:50-14:05

  Coffee Break
  Session 4.

   Chairs: Alexei P. Lisitsa and Andrei P. Nemytykh

 14:05-14:50

    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)

 14:50-15:20

    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 )

 15:20-15:35

  Coffee Break
  Session 5.

   Chair: Lorenzo Clemente

 15:35-16:20

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

 16:20-17:05

    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)

 17:05-17:20

  Coffee Break

  Reminiscences session

 17:20-17:35

    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)

 17:35-17:50

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

 17:50-?18:50?

      Welcome to talk

 ?18:50-19:00?

  Closing

Contacts  
Email:
Alexei Lisitsa, a.lisitsa@csc.liv.ac.uk
Andrei P. Nemytykh, nemytykh@math.botik.ru

Web: http://refal.botik.ru/vpt/vpt2021/
         https://etaps.org/2021/workshops/