Published: 13th September 2021|
|An Overview of the HFL Model Checking Project Naoki Kobayashi||1|
|Termination Analysis of Programs with Multiphase Control-Flow Jesús J. Domenech and Samir Genaim||13|
|Regular Path Clauses and Their Application in Solving Loops Bishoksan Kafle, John P. Gallagher, Manuel V. Hermenegildo, Maximiliano Klemen, Pedro López-García and José F. Morales||22|
|Reducing Higher-order Recursion Scheme Equivalence to Coinductive Higher-order Constrained Horn Clauses Jerome Jochems||36|
|A Fixed-point Theorem for Horn Formula Equations Stefan Hetzl and Johannes Kloibhofer||65|
|Knowledge-Assisted Reasoning of Model-Augmented System Requirements with Event Calculus and Goal-Directed Answer Set Programming Brendan Hall, Sarat Chandra Varanasi, Jan Fiedor, Joaquín Arias, Kinjal Basu, Fang Li, Devesh Bhatt, Kevin Driscoll, Elmer Salazar and Gopal Gupta||79|
|Competition Report: CHC-COMP-21 Grigory Fedyukovich and Philipp Rümmer||91|
This volume contains revised and extended versions of papers and invited talks presented at the 8th workshop on Horn Clauses for Verification and Synthesis (HCVS), which took place virtually on 28 March, 2021 due to COVID-19 pandemic as an affiliated workshop of ETAPS. The aim of the HCVS workshop series is to stimulate and promote international research and collaboration by bringing together the CLP and CAV communities on efficiently solving program verification and synthesis problems presented as constrained Horn clauses (CHCs). The included papers illustrate CHCs as a common representation for specifying and verifying program properties and also for implementing practical tools based on this.
We would like to thank the editorial office of EPTCS, in particular editor-in-chief Rob van Glabbeek for his help and support in hosting this event. Our sincere thanks to the program committee and steering committee members (especially Fabio Fioravanti) of HCVS, and local organizers of ETAPS and to the reviewers of the papers for their support and hard work.