Proceedings of the Fourth International Workshop on Verification and Program Transformation

TL;DR

This paper summarizes the proceedings of the VPT 2016 workshop, highlighting the interdisciplinary exchange between program verification and transformation methods, and their mutual benefits in advancing software analysis techniques.

Contribution

It provides an overview of recent research that integrates program transformation and verification methods, demonstrating their combined effectiveness in system analysis.

Findings

Transformation techniques aid in verifying infinite state systems.

Verification methods enhance program transformation tools.

Interdisciplinary approaches improve software analysis capabilities.

Abstract

This volume contains the revised versions of papers presented at the Fourth International Workshop on Verification and Program Transformation (VPT 2016) on April 2, 2016 in Eindhoven, The Netherlands. The workshop is an event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2016). The aim of the VPT workshops is to provide a forum where people from the area of program transformation and the area of program verification can fruitfully exchange ideas and gain a deeper understanding of the interactions between those two fields. The research papers which have been recently published in those fields, show that the interactions are very beneficial and, indeed, go both ways. In one direction, methods and tools developed in the field of program transformation, such as partial deduction, partial evaluation, fold/unfold transformations, and supercompilation, have all been applied with success for the verification of systems, and in particular, the verification of infinite state and parameterized systems. In the other direction, methods developed in program verification, such as model checking, abstract interpretation, SAT and SMT solving, and automated theorem proving, have been used to enhance program transformation techniques, thereby making these techniques more powerful and useful in practice.