Programme
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:

Demer and Saint Catherine Church John P. Gallagher Igor Walukiewicz Dániel Horpácsi Geoff Hamilton Bishoksan Kafle Antonina Nepeivoda Gergö Barany Julien Cohen Venkatesh Kannan Nature vs. abstraction. What do you prefer?

The VPT-2016 Proceedings has been published as Volume 216 of Electronic Proceedings in Theoretical Computer Science.

Programme

   Saturday, April 2

  Registration will take place in the Auditorium.

The Auditorium / Room: CZ 13 (upstairs)

 09:00-09:15

  Opening

 09:15-10:00

    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)

 10:00-10:30

    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 )

 10:30-11:00

  Coffee Break

 11:00-11:30

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

 11:30-12:00

    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 )

 12:00-12:30

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

 12:30-14:00

  Lunch

 14:00-14:45

    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)

 14:45-15:15

    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 )

 15:15-15:45

  Coffee Break

 15:45-16:15

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

 16:15-16:45

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

 16:45-17:15

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

 17:15-18:00

  Discussion and Closing

Contacts  
Email:
Geoff W. Hamilton, hamilton@computing.dcu.ie
Alexei Lisitsa, a.lisitsa@csc.liv.ac.uk
Andrei P. Nemytykh, nemytykh@math.botik.ru

Web: http://refal.botik.ru/vpt/vpt2016/
         http://www.etaps.org/index.php/2016/workshops?id=260#VPT