VPT 2013 / Program

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.

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.

4:35-5:10

Abdulbasit Ahmed, Alexei Lisitsa and Andrei Nemytykh. Cryptographic Protocol Verification via Supercompilation (A Case Study).

   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.

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.

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.

Dominique Mery and Rosemary Monahan. Transforming Event B Models into Verified C# Implementations.

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/

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.
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.
4:35-5:10	Abdulbasit Ahmed, Alexei Lisitsa and Andrei Nemytykh. Cryptographic Protocol Verification via Supercompilation (A Case Study).

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.
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.
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. Dominique Mery and Rosemary Monahan. Transforming Event B Models into Verified C# Implementations.