Preface

This volume contains the proceedings of the Third International Workshop on Verification and Program Transformation (VPT 2015). The workshop took place in London, UK, on 11th of April 2015. Previous editions of the Workshop were held at Saint-Petersburg (Russia) in 2013, and Vienna (Austria) in 2014.

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.

The programme committee received 10 submissions and selected 6 of them for regular presentation and 2 of them for short presentation at the workshop. Each paper was revised by at least two referees, and the selection was based on originality, quality, and relevance to the topics of the call for papers. The speakers were invited for submitting revised versions of the presented papers for the formal post-proceedings of the workshop. The revised versions underwent a second referee process and 5 of them were selected for publication in these post-proceedings.

The scientific programme included papers on verification by transformation, control flow analysis, and finite countermodel based verification. Additionally, two invited talks were given by Arie Gurfinkel (Software Engineering Institute, Carnegie Mellon University, USA) and David Monniaux (VERIMAG, CNRS - University of Grenoble, France). Arie Gurfinkel illustrated the functionalities of a verification framework, called SeaHorn, and David Monniaux spoke about the various ways in which program transformation and program verification are fruitfully interrelated.

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 like to thank Paulo Oliva (Queen Mary University of London, U.K.) for his help in making the event possible. Our thanks go also to Emanuele De Angelis (University of Chieti-Pescara, Italy) who assisted us in the many organizational matters. Finally, we warmly thank the EasyChair organization for supporting the various tasks related to the selection of the contributions, and also EPTCS and arXiv for hosting the proceedings.

October 2015,
Alexei Lisitsa, Andrei Nemytykh, and Alberto Pettorossi.

Programme Committee

Santiago Escobar, Technical University of Valéncia, Spain
Fabio Fioravanti, University of Chieti-Pescara, Italy
John Gallagher, Roskilde University, Denmark
Silvio Ghilardi, University of Milano, Italy
Geoff W. Hamilton, Dublin City University, Republic of Ireland
Michael Hanus, University of Kiel, Germany
Andy King, University of Kent, UK
Michael Leuschel, Heinrich-Heine-Universität Düsseldorf, Germany
Alexei Lisitsa, The University of Liverpool, UK (co-chair)
Andrei P. Nemytykh, Program Systems Institute of RAS, Russia (co-chair)
Alberto Pettorossi, University of Roma Tor Vergata, Italy (co-chair)
Germán Vidal, Technical University of Valéncia, Spain

We tackle the problem of verifying behavioural equivalence of refactorings by 1) providing an abstract representation for Simulink models in the form of equations that express the relation between ingoing and outgoing signals at the blocks, 2) proving the soundness of the abstract representation by relating it to an operational semantics of Simulink's simulation engine, 3) adapting the notion of approximate bisimulation to Simulink models, which allows values of equivalent steps of source and target model to be ‘close’ to each other rather than being identical as in bisimulation, and 4) providing a methodology for proving the approximate bisimulation for refactorings for three kinds of Simulink models - unsampled (models without discrete or continuous blocks), discrete, and continuous systems. While we consider ‘exact’ equivalence for the first two kinds of systems, for the latter kind of systems, we provide an epsilon ‘tube’ for the precision of the approximate bisimulation in the simulation interval.

The scenario for our approach is the following. Suppose that a user wants to refactor a Simulink model. This is only admissible if the behaviour of source and target model is equivalent. Our approach constitutes a first step towards a framework that enables the user to verify the (approximate) behavioural equivalence of source and target Simulink model. In this context, the representation of Simulink models as equations allows us to abstract from the details of the operational semantics and to verify approximate semantical equivalence on the basis of a syntactical comparison of these equations. Examples for refactorings that we currently support are 1) arithmetic equivalences for the unsampled case, 2) substitution of several unit delay blocks for the discrete case, and 3) substitution of a system that describes a set of ordinary differential equations by a system that expresses the analytical solution directly.

In future work, we aim at automating our approach. We also strive for covering hybrid models, i.e., models that contain both, discrete and continuous blocks. Furthermore, we plan to improve the precision of the epsilon tube that can get larger depending on the size of the simulation interval in the general case by considering more advanced approximation techniques from Simulink and taking stability theory into account. To obtain the full paper, please contact the authors.