Preface

This volume contains the joint post-proceedings of the 9th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2022) and the 10th Workshop on Verification and Program Transformation (VPT 2022), which took place in Munich, Germany on April 3, 2022, as affiliated workshops of the European Joint Conferences on Theory and Practice of Software (ETAPS). The two workshops were held in-person, also allowing virtual attendance and some remote presentations. The attendance on site was quite good, gathering over 20 participants.

HCVS and VPT are both concerned with formal reasoning for program verification, transformation and synthesis. The workshops topics and communities have a significant overlap, and it has been very natural to merge them into a single event.

HCVS 2022 follows previous meetings: HCVS 2021 in Luxembourg, Luxembourg (ETAPS 2021), HCVS 2020 (cancelled as an in-person workshop of ETAPS 2020 due to COVID, papers published in conjunction with VPT 2020), HCVS 2019 in Prague, Czech Republic (ETAPS 2019), HCVS 2018 in Oxford, UK (CAV, ICLP and IJCAR at FLoC 2018), HCVS 2017 in Gothenburg, Sweden (CADE 2017), HCVS 2016 in Eindhoven, The Netherlands (ETAPS 2016), HCVS 2015 in San Francisco, CA, USA (CAV 2015), and HCVS 2014 in Vienna, Austria (VSL).

Many Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses and many recent advances in the CLP and CAV communities have centered around efficiently solving problems presented as Horn clauses. The HCVS series of workshops aims to bring together researchers working in the communities of Constraint/Logic Programming (e.g., ICLP and CP), Program Verification (e.g., CAV, TACAS, and VMCAI), and Automated Deduction (e.g., CADE, IJCAR), on the topic of Horn clause based analysis, verification, and synthesis.

HCVS 2022 hosted the 5th competition on constraint Horn clauses (CHC-COMP), which compares state-of-the-art tools for CHC solving for performance and effectiveness on a set of publicly available benchmarks. A report on the 5th CHC-COMP is part of these proceedings. The report also contains tool descriptions of the participating solvers.

VPT 2022 is the tenth in the series after VPT 2021 in Luxembourg, Luxembourg (ETAPS 2021), VPT 2020 (postponed in-line with ETAPS 2020, but held in conjunction with VPT 2021), VPT 2019 in Genova, Italy (Programming 2019), VPT 2018 in Thessaloniki, Greece (ETAPS 2018), VPT 2017 in Uppsala, Sweden (ETAPS 2017), VPT 2016 in Eindhoven, Netherlands (ETAPS 2016), VPT 2015 in London, UK (ETAPS 2015), VPT 2014 in Vienna, Austria (CAV/VSL 2014) and VPT 2013 in St. Petersburg, Russia (CAV 2013).

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 recently published in these 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 and fold/unfold transformations have all been applied with success in 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.

This volume includes only a subset of the work presented at the joint workshops. The papers published here are full versions of abstract or extended abstracts that were submitted after the workshop and reviewed by the Program Committee. For completeness of information, we report below the full program of the event. More information can be found on the workshops web page https://www.sci.unich.it/hcvs22/program.html.

We wish to thank the authors who submitted papers, the speakers, the invited speakers, the program committee members, and the additional reviewers for the work they have generously done. We would also like to thank Jan Křetínský (LMU Munich, ETAPS 2022 general co-chair) and Dirk Beyer (LMU Munich, ETAPS 2022 general co-chair and workshops chair), who provided invaluable support to the workshop organizers. Finally, we warmly thank EasyChair for supporting the submission and selection of the contributions, and also EPTCS, and in particular the editor-in-chief Rob van Glabbeek, for hosting these proceedings.

October 2022,
Geoffrey Hamilton, Temesghen Kasai, Maurizio Proietti

HCVS 2022 Program Committee

Elvira Albert, Complutense University of Madrid, Spain

Emanuele De Angelis, IASI-CNR, Italy

Grigory Fedyukovich, Florida State University, USA

Fabio Fioravanti, University of Chieti-Pescara, Italy

Arie Gurfinkel, University of Waterloo, Canada

Bishoksan Kafle, IMDEA Software Institute, Spain

Temesghen Kahsai, Amazon, USA (co-chair)

Naoki Kobayashi, University of Tokyo, Japan

Ekaterina Komendantskaya, Heriot-Watt University, UK

Annie Liu, Stony Brook University, USA

Dale Miller, Inria Saclay & LIX, France

Jorge A. Navas, Certora, USA

Saswat Padhi, Amazon, USA

Maurizio Proietti, IASI-CNR, Italy (co-chair)

Philipp Rüemmer, Uppsala University, Sweden

Mattias Ulbrich, Karlsruhe Institute of Technology, Germany

External Reviewers

Alejandro Hernández-Cerezo, Hossein Hojjat, Alberto Pettorossi.

VPT 2022 Program Committee

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 (Chair)

Michael Hanus, University of Kiel, Germany

Marie-Christine Jakobs, Ludwig-Maximilians-Universitat, Munchen, Germany

Alexei Lisitsa, The University of Liverpool, UK

Andrei P. Nemytykh, Program Systems Institute of RAS, Russia

Maurizio Proietti, IASI-CNR, Rome, Italy

Gabriel Radanne, IRIF, Inria, Paris, France

Philipp Rümmer, Uppsala University, Sweden

Germán Vidal, Technical University of Valéncia, Spain

Program of joint HCVS & VPT 2022