Published: 6th September 2021|
|Preface Alexei Lisitsa and Andrei P. Nemytykh|
|Invited Paper: Conjectures, Tests and Proofs: An Overview of Theory Exploration Moa Johansson and Nicholas Smallbone||1|
|Improving Dynamic Code Analysis by Code Abstraction Isabella Mastroeni and Vincenzo Arceri||17|
|An Inversion Tool for Conditional Term Rewriting Systems - A Case Study of Ackermann Inversion Maria Bendix Mikkelsen, Robert Glück and Maja H. Kirkeby||33|
|Program Specialization as a Tool for Solving Word Equations Antonina Nepeivoda||42|
|An Empirical Study of Partial Deduction for miniKanren Ekaterina Verbitskaia, Daniil Berezun and Dmitry Boulytchev||73|
This volume contains the proceedings of the Ninth International Workshop on Verification and Program Transformation (VPT 2021) which was held online on March 27th and 28th as a part of a joint event, together with the VPT 2020 workshop, co-located with the ETAPS 2021 conference.
The previous VPT 2020 workshop was organized in honour of Professor Alberto Pettorossi on the occasion of his academic retirement from Università di Roma Tor Vergata. Due to the pandemic the VPT 2020 meeting was cancelled but its proceeding have already appeared in the EPTCS 320 volume.
The joint VPT-20-21 event has subsumed the original programme of VPT 2020 and provided an opportunity to meet and celebrate the achievements of Professor Alberto Pettorossi; its programme was further expanded with the newly submitted presentations for VPT 2021.
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 event has attracted many invited talks following a keynote speech by Alberto Pettorossi. The corresponding Invited Speakers were Lorenzo Clemente (U. Warsaw), Agostino Cortesi (U. Ca' Foscari, Venezia), John P. Gallagher (Roskilde U. & IMDEA Software Institute), Nikos Gorogiannis (Facebook London), Fritz Henglein (U. Copenhagen & Deon Digital), Moa Johansson (Chalmers U., Gothenburg), Neil D. Jones (U. Copenhagen), Benjamin Kaminski (U. College London), Laura Kovacs (Vienna U. of Technology), Michael Leuschel (Heinrich-Heine U.), Michael Norrish (Australian National U.) and Maurizio Proietti (IASI-CNR).
Additionally to the VPT 2020 contributed talks the VPT 2021 program committee accepted four submissions that have been presented at the joint workshop and which are included in these proceedings. Each submission was reviewed by four or more referees, and the selection was based on originality, quality, and relevance to the topics of the call for papers. The proceeding contains also an invited paper by Moa Johansson and Nicholas Smallbone.
The editors would like to warmly thank the authors of these contributions, as well as the members of the PC of VPT 2021 for their constructive reviews of the regular papers.
The editors wish to express our gratitude to the authors who submitted papers, the speakers, the keynote and invited speakers, and the program committee members for the work they have generously done. We would like to thank Laurent Fribourg, the VPT 2020 PC chair, whose great effort was the main organizing contribution in the success of this joint workshop. We warmly thank Maurizio Proietti for his enormous help in attracting the invited speakers.
We would like to thank the ETAPS workshops Chair Joaquin Garcia-Alfaro, organization Chair Peter Roenne and Magali Martin 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 publisher for its final help with the publication, and arXiv for hosting the proceedings.
Alexei Lisitsa, and Andrei Nemytykh