Third International Workshop on
Verification and Program Transformation

The Third International Workshop on Verification and Program Transformation (VPT-2015) aims to bring together researchers working in two different areas, Verification and Program Transformation. VPT 2015 will be an ETAPS 2015 Workshop, and held on April 11th, 2015, London, UK.

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-2015 Proceedings has been published as Volume 199 of Electronic Proceedings in Theoretical Computer Science.


   Saturday, April 11



Francis Bancroft Building / Room: FB.1.01.2




    Arie Gurfinkel (Software Engineering Institute, Carnegie Mellon University, USA). The SeaHorn Verification Framework. Arie_Gurfinkel_VPT-2015_abstract.pdf (slides: VPT2015-Gurfinkel_presentation.pdf , pptx )  (Invited talk)


    Martin Lester. Control Flow Analysis for SF Combinator Calculus. (preprint VPT2015_preprint_4.pdf , slides: VPT2015-Martin_Lester-mml_presentation.pdf )


  Coffee Break


    Bishoksan Kafle, John P. Gallagher and Pierre Ganty. Decomposition by Tree Dimension in Horn Clause Verification. (preprint VPT2015_preprint_10.pdf , slides: VPT2015-Gallagher-Kafle-Ganty_presentation.pdf )


    G.W. Hamilton. Verifying Temporal Properties of Reactive Systems by Transformation. (preprint VPT2015_preprint_3.pdf , slides: VPT2015-Hamilton_presentation.pdf )






    David Monniaux (VERIMAG, CNRS - University of Grenoble, France). Program Transformation and Verification are Interrelated. David_Monniaux_VPT-2015_abstract.pdf (slides: VPT2015-DMonniaux_transformation_analysis.pdf )  (Invited talk)


    Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti. Proving Horn Clause Specifications of Imperative Programs. (preprint VPT2015_preprint_8.pdf , slides: VPT2015-Proietti-De_Angelis-Fioravanti-Pettorossi_presentation.pdf )


    Wei Bai and Emmanuel M. Tadjouddine. Automated Program Translation in Certifying Online Auctions. (preprint VPT2015_preprint_5.pdf )




  Coffee Break


    Alexei P. Lisitsa and Andrei P. Nemytykh. Finite Countermodel Based Verification for Program Transformation (A Case Study). (preprint VPT2015_preprint_1.pdf , slides: VPT2015-Lisitsa-Nemytykh_presentation.pdf )


    Sebastian Schlesinger, Paula Herber, Thomas Gothel and Sabine Glesner. Towards the Verification of Refactorings of Hybrid Simulink Models. (Presentation, preprint VPT2015_abstract_preprint_7.pdf , slides: VPT2015-Schlesinger-Herber-Gothel-Glesner_presentation.pdf )


    Fouad ben Nasr Omri, Safa Omri and Ralf Reussner. Incremental and Compositional Probabilistic Analysis of Programs under Uncertainty. (Presentation, preprint VPT2015_abstract_preprint_9.pdf )



Emanuele De Angelis,
Alexei Lisitsa,
Andrei P. Nemytykh,
Alberto Pettorossi,