Published: 20th August 2019
DOI: 10.4204/EPTCS.299
ISSN: 2075-2180

EPTCS 299

Proceedings Seventh International Workshop on
Verification and Program Transformation
Genova, Italy, 2nd April 2019

Edited by: Alexei Lisitsa and Andrei Nemytykh

Preface
Alexei Lisitsa and Andrei P. Nemytykh
Invited Presentation: Modelling and Verifying Bitcoin Contracts (Invited Talk)
Massimo Bartoletti
1
Invited Presentation: Validation of Internet of Things Frameworks (Invited Talk)
Giorgio Delzanno
2
Invited Presentation: Hacking Program Analysis: A Systematic Approach to Code Protection (Invited Talk)
Roberto Giacobazzi
3
Lemma Generation for Horn Clause Satisfiability: A Preliminary Study
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti
4
Static Program Analysis for String Manipulation Languages
Vincenzo Arceri and Isabella Mastroeni
19
Polyvariant Program Specialisation with Property-based Abstraction
John P. Gallagher
34
Iteratively Composing Statically Verified Traits
Isaac Oscar Gariano, Marco Servetto, Alex Potanin and Hrshikesh Arora
49

Preface

This volume contains the proceedings of the Seventh International Workshop on Verification and Program Transformation (VPT 2019), which took place in Genova, Italy, on April 2nd, 2019, affiliated with Programming 2019. Previous editions of the Workshop were held in Saint-Petersburg (Russia, affiliated with CAV 2013), Vienna (Austria, affiliated with CAV 2014), London (UK, affiliated with ETAPS 2015), Eindhoven (The Netherlands, affiliated with ETAPS 2016), Uppsala (Sweden, affiliated with ETAPS 2017) and Thessaloniki (Greece, affiliated with ETAPS 2018, co-located with MARS 2018).

The aim of the VPT workshop series is to provide a forum where people from the areas of program transformation and 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 software 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 program committee received nine submissions and selected six of them for presentation at the workshop. Each paper was revised by three or more referees, and the selection was based on originality, quality, and relevance to the topics of the call for papers. Four contributions are published as papers in this volume. One selected submission was not presented at the workshop. Additionally, there were the following three invited talks:

We wish to express our gratitude to the authors who submitted papers, the speakers, the invited speakers, and the program committee members for the work they have generously done. We would like to thank the Programming-2019 workshops chairs Walter Cazzola (Università degli Studi di Milano, Italy) and Stefan Marr (University of Kent, UK) for their help in making the event possible. 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. The workshop was partially supported by:


July 2019,
Alexei Lisitsa, and Andrei Nemytykh.

Organizing Committee

Alexei Lisitsa, The University of Liverpool, UK
Andrei P. Nemytykh, Program Systems Institute of RAS, Russia

Programme Committee

Amir Ben-Amram, Academic Colledge of Tel-Aviv-Yaffo, Israel
Grigory Fedyukovich, Princeton University, USA
John P. Gallagher, Roskilde University, Denmark, and IMDEA Software Institute, Spain
Geoff W. Hamilton, Dublin City University, Republic of Ireland
Oleg Kiselyov, Tohoku University, Japan
Alexei Lisitsa, The University of Liverpool, UK (co-chair)
Andrei P. Nemytykh, Program Systems Institute of RAS, Russia (co-chair)
Alberto Pettorossi, Universita di Roma Tor Vergata, Italy
Maurizio Proietti, IASI-CNR, Rome, Italy
Andrey Rybalchenko, Microsoft Research, Cambridge, UK
Kostis Sagonas, Uppsala University, Sweden
Peter Sestoft, The IT University of Copenhagen, Denmark

Steering Committee

Geoff W. Hamilton, Dublin City University, Republic of Ireland
Alexei Lisitsa, The University of Liverpool, UK
Andrei P. Nemytykh, Program Systems Institute of RAS, Russia
Alberto Pettorossi, Università di Roma Tor Vergata, Italy


Modelling and Verifying Bitcoin Contracts (Invited Talk)

Massimo Bartoletti (University of Cagliari, Italy)

Albeit the primary usage of Bitcoin is to exchange currency, its blockchain and consensus mechanism can also be exploited to securely execute some forms of smart contracts. These are agreements among mutually distrusting parties, which can be automatically enforced without resorting to a trusted intermediary. However, the existing informal, low-level descriptions, and the use of poorly documented Bitcoin features, pose obstacles to the research in this field. To overcome these issue we have recently proposed BitML, a high-level DSL for smart contracts with a computationally sound compiler to Bitcoin transactions. In this talk we start from BitML to investigate a landmark property of contracts, called liquidity: in a non-liquid contract, it may happen that some funds remain frozen. Liquidity is a relevant issue, as witnessed by a recent attack to the Ethereum Parity Wallet, which has frozen ~160M USD within the contract, making this sum unredeemable by any user.

We develop a verification technique for liquidity of BitML contracts. To prove this, we first transform the infinite-state semantics of BitML into a finite-state one, which focusses on the behaviour of any given set of contracts, abstracting the moves of the context. With respect to the chosen contracts, this abstraction in sound and complete. Our decision procedure for liquidity is then based on model-checking the finite space of states of the abstraction.


Validation of Internet of Things Frameworks (Invited Talk)

Giorgio Delzanno (DIBRIS, Università di Genova, Italy)

IoT systems are distributed systems involving heterogenous components (devices, servers, cloud services, … ). In this setting IoT applications are often based on event-driven asynchronous programming frameworks such as Node.js.

In the talk I will present different approaches (from verification to testing) that can be combined to validate applications developed in this complex scenario.


Hacking Program Analysis: A Systematic Approach to Code Protection (Invited Talk)

Roberto Giacobazzi (Università di Verona, Italy)

The talk concerns the design of code protecting transformations for anti reverse engineering applications. This is a gentle introduction for non-specialists to some of the results and studies I made in the last years on the limits and possibilities of making analyses imprecise by systematic code transformation. These technologies are widely used in code protection (e.g., IP protection or key protection), malware design, anti tampering, code watermarking and birth-marking of code. The battle scenario involves attackers intended to extract information by reverse engineering the code, and protecting code transformations modeled as distorted compilers devoted to inhibit these attacks. Attacks are inhibited by maximizing imprecision in all attempts made by the attacker to exploit control and data-flow of the obscured code. After a brief survey on the state of the art in the field, we introduce a model for code obfuscation which is general enough to include generic automated static and dynamic attacks. Protecting transformations are then systematically and formally derived as distorted compilers, obtained by specializing a suitably distorted interpreter for the given programming language with respect to the source code to protect. The limits of these methods are shown in the context of computational theory. Interestingly this distortion corresponds precisely to defeat the potency of the expected attacker, which is itself an interpreter and whose potency consists in its ability to extract a complete and precise view of program's execution.