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:

The VPT-2021 Proceedings have been published as Volume 341 of Electronic Proceedings in Theoretical Computer Science.

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 , YouTube: Alberto-Pettorossi-VPT-2021_record , Zoom: Alberto-Pettorossi-VPT-2021_record ) (Keynote speech)

 10:00-10:15

  Coffee Break  (The two records at the second session: Zoom: Maurizio_Proietti-and-Lorenzo_Clemente-VPT-2021_records )

 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 , YouTube: Maurizio_Proietti-VPT-2021_records ) (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 , YouTube: Lorenzo_Clemente-VPT-2021_records ) (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 , Zoom: John_P_Gallagher-VPT-2021_record ) (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 , Zoom: Horatiu_Cirstea-VPT-2021_record )

 14:00-14:15

  Coffee Break
  Session 4.

   Chair: Fritz Henglein  (The two records at the fourth session: Zoom: Siddharth_Bhaskar-and-Dimitur_Krustev-VPT-2021_records )

 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 , YouTube: Dimitur_Krustev-VPT-2021_records )

 15:30-15:45

  Coffee Break
  Session 5.

   Chair: John P. Gallagher  (The first and second records at the fifth session: Zoom: Moa_Johansson-and-Geoff_W_Hamilton-VPT-2021_records )

 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 , YouTube: Moa_Johansson-VPT-2021_records )  (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 , YouTube: Geoff_W_Hamilton-VPT-2021_record )

 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 , YouTube: Michael_Leuschel-VPT-2021_record , Zoom: Michael_Leuschel-VPT-2021_record ) (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                        (The two records at the first session and the two records at the second session: Zoom: Michael_Norrish-and-Isabella-Mastroeni-and-Agostino_Cortesi-and-Maria_Bendix_Mikkelsen-VPT-2021_records )
  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 , YouTube: Michael_Norrish-VPT-2021_record )   (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 , YouTube: Michael_Norrish-VPT-2021_record )   (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  (The two records at the third session: Zoom: Nikos_Gorogiannis-and-Antonina_Nepeivoda-VPT-2021_records )

 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 , YouTube: Michael_Norrish-VPT-2021_record )

 13:50-14:05

  Coffee Break
  Session 4.

   Chairs: Alexei P. Lisitsa and Andrei P. Nemytykh  (The two records at the fourth session: Zoom: Fritz_Henglein-and-Ekaterina_Verbitskaia-VPT-2021_records )

 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 , YouTube: Michael_Norrish-VPT-2021_record )

 15:20-15:35

  Coffee Break  (The two records at the fifth session and the records at Reminiscences session: Zoom: Benjamin_Kaminski-and-Laura_Kovacs-VPT-2021_records )

  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 , YouTube: Michael_Norrish-VPT-2021_record )  (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/

refal.botik.ru/vpt/vpt2021/Ib5kFpgmVPT20219Hf5vurliRcgyvIlkxugP8zCZ5B4hWdjliTNA83hubMwCZZsXjbPSCP4