Programme
Second International Workshop on
Verification and Program Transformation


The Second International Workshop on Verification and Program Transformation (VPT-2014) aims to bring together researchers working in two different areas, Verification and Program Transformation. VPT 2014 will be an event of the Vienna Summer of Logic 2014 and a CAV 2014 Workshop, and held on July 17th and 18th, 2014.

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-2014 Proceedings has been published as Volume 28 of EasyChair proceedings.

Programme

   Thursday, July 17

 10:45-10:50

  Openning

 10:50-11:30

    Antonina Nepeivoda. Verification of Multi-Party Ping-Pong Protocols via Program Transformation. Antonina-Nepeivoda_VPT-2014_talk.pdf

 11:30-12:15

    Daniil Frumin and Irina Lomazova. Branching Processes of Conservative Nested Petri Nets. Frumin_Lomazova_VPT-2014_talk.pdf

 12:15-13:00

    Alexei Lisitsa and Andrei Nemytykh. A Note on Program Specialization. What Syntactical Properties of Residual Programs Can Reveal? Lisitsa_Nemytykh_VPT-2014_talk.pdf

 13:00-14:30

  Lunch

 14:30-15:30

    Invited Talk (shared with HCSV): Michael Leuschel (Heinrich-Heine-Universität Düsseldorf). Towards Constraint-Solving over Higher-Order Unbounded Datatypes using Formal Methods Tools.

 16:00-16:30

  Coffee Break

   Friday, July 18

 9:15-10:15

    Invited Talk: Klaus von Gleissenthall, Andrey Rybalchenko (Microsoft Research) and Santiago Zanella-Béguelin. Towards Automated Proving of Relational Properties of Probabilistic Programs.

 10:15-10:45

  Coffee Break

 10:45-11:30

    Andrei Nemytykh. On Unfolding for Programs Using Strings as a Data Type. Nemytykh_VPT-2014_talk.pdf

 11:30-12:15

    Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti. Program Verification using Constraint Handling Rules and Array Constraint Generalizations. DeAngelis-et-al_VPT-2014_talk.pdf

 12:15-13:00

    Geoff Hamilton and Morten Heine Sørensen. Local Driving in Higher-Order Positive Supercompilation via the Omega-theorem.

 13:00-14:30

  Lunch

 14:30-18:00

  Joint session with WWV

 14:30-15:15

    Invited Talk (shared with WWV): Josep Silva (Universidad Politécnica de Valencia). Automatic Detection of Webpage Candidates for Site-Level Web Template Extraction.

 15:15-16:00

    Invited Talk (shared with WWV): Steve Ross-Talbot (Cognizant Technology Solutions, United Kingdom). A Formal Approach to Legacy Modernization: Baby Steps.

 16:00-16:30

  Coffee Break

 16:30-17:00

    Thomas Sewell. Formal Replay of Translation Validation for Highly Optimised C.

 17:00-17:30

    R. Ramanujam and S. Sheerazuddin. A Local Logic for Realizability in Web Service Choreographies.

 17:30-18:00

    Asad Ali and Maribel Fernandez. Static Enforcement of Role-Based Access Control.

Invited and regular papers accepted for presentation at the workshop appear as Volume 28 of the EasyChair Proceedings in Computing (EPiC) series. The VPT-2014 Proceedings has been published as Volume 28 of EasyChair proceedings.

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