Programme
First International Workshop on
Verification and Program Transformation


The First International Workshop on Verification and Program Transformation (VPT-2013) aims to bring together researchers working in two different areas, Verification and Program Transformation. VPT 2013 will be a CAV 2013 Workshop and held on July 13th and 14th, 2013.

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:
See the following page for higher resolution versions of these pictures.

The VPT-2013 Proceedings has been published as Volume 16 of EasyChair proceedings.

Programme

   Saturday, July 13

 9:25-9:30

  Openning

 9:30-10:30

    Invited Talk: Alberto Pettorossi (DICII, University of Rome Tor Vergata) and Maurizio Proietti (IASI-CNR, Rome). Program Transformation for Program Verification.

 10:30-11:00

  Coffee Break

 11:00-11:55

    Invited Talk: Amir M. Ben-Amram (The Academic College of Tel-Aviv Yaffo). Ranking Functions for Linear-Constraint Loops.

 11:55-12:30

    Geoff W. Hamilton. On the Termination of Higher-Order Positive Supercompilation. Hamilton_VPT-2013_talk.pdf

 12:30-2:00

  Lunch

 2:00-3:00

    Invited Talk: Jérôme Leroux (LaBRI, Université de Bordeaux, CNRS). Acceleration For Presburger Petri Nets.

 3:00-3:30

    Discussion

 3:30-4:00

  Coffee Break

 4:00-4:35

    Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti. Verification of Imperative Programs through Transformation of Constraint Logic Programs. Angelis_Fioravanti_Pettorossi_Proietti_VPT-2013_talk.pdf

 4:35-5:10

    Abdulbasit Ahmed, Alexei Lisitsa and Andrei Nemytykh. Cryptographic Protocol Verification via Supercompilation (A Case Study). Ahmed_Lisitsa_Nemytykh_VPT-2013_talk.pdf

   Sunday, July 14

 9:30-10:30

    Invited Talk: Bernd Finkbeiner (Universität des Saarlandes). Transforming Undecidable Synthesis Problems into Decidable Problems.

 10:30-11:00

  Coffee Break

 11:00-12:00

    Invited Talk: Simon Thompson (School of Computing, University of Kent). Building Trustworthy Refactoring Tools. Thomson_Arts_Drienyovszky_Horpacsi_Li_Sultana_VPT-2013_talk.pdf

 12:00-12:30

    Discussion

 12:30-2:00

  Lunch

 2:00-2:35

    Presentation only: Ondrej Sery, Grigory Fedyukovich and Natasha Sharygina. Incremental Upgrade Checking by Means of Interpolation-based Function Summaries.

 2:35-3:10

    Antonina Nepeivoda. Ping-Pong Protocols as Prefix Grammars and Turchin Relation. Antonina-Nepeivoda_VPT-2013_talk.pdf

 3:10-3:30

    Discussion

 3:30-4:00

  Coffee Break

 4:00-5:00

  • Presentation only: Andrei Nemytykh. Graphical Tracing of Supercompilation: An Intermediate Report. Nemytykh_VPT-2013_talk.pdf

  • Dominique Mery and Rosemary Monahan. Transforming Event B Models into Verified C# Implementations. Mery_Monahan_VPT-2013_talk.pdf

We have plenty of time for discussion.

Invited and regular papers accepted for presentation at the workshop appear as Volume 16 of the EasyChair Proceedings in Computing (EPiC) series.

A formal workshop Pre-Proceedings will be published at a local publishing house before the workshop. This printed Pre-Proceedings and an electronic version of the workshop Proceedings will be distributed on a USB sticks at the workshop. The VPT-2013 Proceedings has been published as Volume 16 of EasyChair proceedings.

Contacts
Email:
a.lisitsa@csc.liv.ac.uk
nemytykh@math.botik.ru
Web: http://refal.botik.ru/vpt/