Published: 6th July 2016
|Preface Geoff Hamilton, Alexei Lisitsa and Andrei P. Nemytykh
|Invited Talk: Finite Tree Automata in Horn Clause Transformations John P. Gallagher
|Invited Talk: Model Based Approach to Verification of Higher-Order Programs Igor Walukiewicz
|Hybrid Information Flow Analysis for Programs with Arrays Gergö Barany
|Flowchart Programs, Regular Expressions, and Decidability of Polynomial Growth-Rate Amir M. Ben-Amram and Aviad Pineles
|Renaming Global Variables in C Mechanically Proved Correct Julien Cohen
|Generating Counterexamples for Model Checking by Transformation G. W. Hamilton
|Towards Trustworthy Refactoring in Erlang Dániel Horpácsi, Judit Kőszegi and Simon Thompson
|Interpolant Tree Automata and their Application in Horn Clause Verification Bishoksan Kafle and John P. Gallagher
|Program Transformation to Identify List-Based Parallel Skeletons Venkatesh Kannan and G. W. Hamilton
|Turchin's Relation for Call-by-Name Computations: A Formal Approach Antonina Nepeivoda
This volume contains the proceedings of the Fourth International Workshop on Verification and Program Transformation (VPT 2016). The workshop took place in Eindhoven, the Netherlands on 2nd April 2016 as an event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2016). Previous editions of the Workshop were held at Saint-Petersburg (Russia) in 2013, Vienna (Austria) in 2014 and London (UK) in 2015.
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.
There were 10 submissions, of which after each getting at least 3 reviews by Program Committee members, 8 were accepted for presentation at the workshop. The scientific programme includes papers on program refactoring, verification by transformation, program complexity and information flow analysis. Additionally, two talks by the internationally renowned invited speakers John Gallagher (Roskilde University, Denmark and IMDEA Software Institute, Spain) and Igor Walukiewicz (Laboratoire Bordelais de Recherche en Informatique, Université Bordeaux-1, France) were given.
We wish to express our gratitude to the authors who submitted papers, the speakers, the invited speakers, the programme committee members (listed below), and the additional reviewers for the work they have generously done. We would also like to thank Erik de Vink (Department of Mathematics and Computer Science, Eindhoven University of Technology) for his help in making the event possible and the EasyChair organization for supporting the various tasks related to the selection of the contributions and also EPTCS and arXiv for hosting the proceedings.
Geoff Hamilton, Alexei Lisitsa and Andrei P. Nemytykh.
Fabio Fioravanti, University of Chieti-Pescara, Italy
Geoff W. Hamilton, Dublin City University, Republic of Ireland (chair)
Michael Hanus, University of Kiel, Germany
Boris Konev, The University of Liverpool, UK
Michael Leuschel, Heinrich-Heine-Universität Düsseldorf, Germany
Alexei Lisitsa, The University of Liverpool, UK
Andrei P. Nemytykh, Program Systems Institute of RAS, Russia
Maurizio Proietti, IASI-CNR, Rome, Italy
Peter Sestoft, The IT University of Copenhagen, Denmark
Morten H. Sørensen, Formalit, Denmark
Germán Vidal, Technical University of Valéncia, Spain
In this talk we look at the fruitful connections between finite tree automata and Horn clause transformations. Horn clause derivations are finite trees and this leads to a straightforward correspondence between a set of Horn clauses and a finite tree automaton. We explore the role of this connection in Horn clause transformations used in program analysis and verification, including elimination of derivations, decomposition of clauses into sets giving derivations of different tree dimension and generation of multiple versions of predicates.
Higher-order programs manipulate not just data, as first-order programs do, but also other programs. Higher-order features make code shorter, more structured, and more modular. They offer mechanisms to deal with such fundamental issues as scalability in multi-processor architectures, or fault tolerance. In this talk we will present some recent advances in verification of both safety and liveness properties of higher-order programs.
To analyse liveness proprties, we need to consider infinite behaviours of functional programs. We regard programs as constructing a possibly infinite execution tree that represents the order in which atomic operations are executed. This approach faithfully models the control flow of a program, while abstracting from its data part. We then use monadic second-order logic, or equivalently parity automata, to express properties of execution trees. We discuss in what sense this approach encompasses many known program analyses, and how it can be also used for program transformation.