Fourth International Workshop on
Verification and Program Transformation

The Fourth International Workshop on Verification and Program Transformation (VPT-2016) aims to bring together researchers working in two different areas, Verification and Program Transformation. VPT 2016 will be an ETAPS 2016 Workshop, and held on April 2nd, 2016, Eindhoven, The Netherlands.

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


   Saturday, April 2

  Registration will take place in the Auditorium.

The Auditorium / Room: CZ 13 (upstairs)




    John Gallagher (Roskilde University, Denmark and IMDEA Software Institute, Spain). Finite Tree Automata in Horn Clause Transformations. John_Gallagher_VPT-2016_abstract.pdf (slides: VPT2016-Gallagher_presentation.pdf )  (Invited talk)


    Dániel Horpácsi, Judit Kőszegi and Simon Thompson. Towards Trustworthy Refactoring in Erlang. (preprint VPT2016_preprint_4.pdf , slides: VPT2016-Horpacsi-Koszegi-Thompson_presentation-Towards_trustworthy_refactoring_in_Erlang.pdf , pptx )


  Coffee Break


    Geoff Hamilton. Generating Counterexamples for Model Checking by Transformation. (preprint VPT2016_preprint_9.pdf , slides: VPT2016-Hamilton_presentation.pdf )


    Bishoksan Kafle and John P. Gallagher. Interpolant Tree Automata and their Application in Horn Clause Verification. (preprint VPT2016_preprint_10.pdf , slides: VPT2016-Kafle-Gallagher_presentation.pdf )


    Antonina Nepeivoda. Turchin's Relation for Call-by-Name Computations: a Formal Approach. (preprint VPT2016_preprint_7.pdf , slides: VPT2016_Antonina-Nepeivoda_presentation.pdf )




    Igor Walukiewicz (CNRS Bordeaux University, France). Model Based Approach to Verification of Higher-Order Programs. Igor_Walukiewicz_VPT-2016_abstract.pdf (slides: VPT2016-Walukiewicz_presentation_Eindhoven16.pdf )  (Invited talk)


    Amir M. Ben-Amram and Aviad Pineles. Flowchart Programs, Regular Expressions, and Decidability of Polynomial Growth-Rate. (preprint VPT2016_preprint_1.pdf , slides: VPT2016_Ben-Amram_Pineles_presentation.pdf )


  Coffee Break


    Gergö Barany. Hybrid Information Flow Analysis for Programs with Arrays. (preprint VPT2016_preprint_5.pdf , slides: VPT2016-Barany_presentation.pdf )


    Julien Cohen. Renaming Global Variables in C Mechanically Proved Correct. (preprint VPT2016_preprint_2.pdf , slides: VPT2016_Cohen_presentation.pdf )


    Venkatesh Kannan and Geoff Hamilton. Program Transformation to Identify List-Based Parallel Skeletons. (preprint VPT2016_preprint_6.pdf , slides: VPT2016-VKannan-GWHamilton_presentation.pdf )


  Discussion and Closing

Geoff W. Hamilton,
Alexei Lisitsa,
Andrei P. Nemytykh,