News
- Videos of the talks
- Program HCVS 2021
- HCVS registration: All participants (including authors, (invited) speakers) need to register to attend the workshop. Deadlines (which is within a week) and associated fees (for workshop only):
- Early registration: Until 15 March 2021 (25 EUR)
- Late registration: From 16 March 2021 (45 EUR)
- Registration webpage: https://etaps.org/2021/registration
- For issues concerning registration please contact directly to the ETAPS organizer since we have no control over it.
Horn Clauses for Verification and Synthesis
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.
This series of workshops aims to bring together researchers working in the two 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.
Horn clauses for verification and synthesis have been advocated by these communities in different times and from different perspectives and HCVS is organized to stimulate interaction and a fruitful exchange and integration of experiences.
The workshop follows seven previous meetings: HCVS 2020 in Dublin, Ireland (ETAPS 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), HCVS 2016 in Eindhoven, The Netherlands (ETAPS), HCVS 2015 in San Francisco, CA, USA (CAV), and HCVS 2014 in Vienna, Austria (VSL).
Accepted Papers
Regular Papers
- A fixed-point theorem for Horn formula equations Stefan Hetzl and Johannes Kloibhofer
- Reducing Higher-order Recursion Scheme Equivalence to Coinductive Higher-order Constrained Horn Clauses Jerome Jochems
- Regular path clauses and their application in solving loops Bishoksan Kafle, John P. Gallagher, Jose F. Morales, Manuel V. Hermenegildo, Pedro Lopez-Garcia and Maximiliano Klemen
- Knowledge-Assisted Reasoning of Formal Model-Based System Engineering with Event Calculus and Goal-Directed Answer Set Programming Brendan Hall, Sarat Chandra Varanasi and Gopal Gupta
Presentation only Papers
- Incremental and Modular Context-sensitive Analysis Isabel Garcia-Contreras, Jose F. Morales and Manuel V. Hermenegildo
- Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti
- The Extended Theory of Trees and Algebraic (Co)datatypes Fabian Zaiser and C.-H. Luke Ong
- Global Guidance for Local Generalization in Model Checking Hari Govind Vediramana Krishnan, YuTing Chen, Sharon Shoham and Arie Gurfinkel
- Solving Constrained Horn Clauses over ADTs by Finite Model Finding Yurii Kostyukov, Dmitry Mordvinov and Grigory Fedyukovich
Contributed Papers
- CHC-COMP 2021 Report Philipp Rümmer and Grigory Fedyukovich
Aims and Scope
Topics of interest include, but are not limited to the use of Horn clauses, constraints, and related formalisms in the following areas:
- Analysis and verification of programs and systems of various kinds (e.g., imperative, object-oriented, functional, logic, higher-order, concurrent, transition systems, petri-nets, smart contracts)
- Program synthesis
- Program testing
- Program transformation
- Constraint solving
- Type systems
- Machine learning and automated reasoning
- CHC encoding of analysis and verification problems
- Resource analysis
- Case studies and tools
- Challenging problems
CHC Competition
HCVS 2021 will host the 4th competition on constraint Horn clauses ( CHC-COMP ), which will compare state-of-the-art tools for CHC solving for performance and effectiveness on a set of publicly available benchmarks. A report on the 4th CHC-COMP will be part of the workshop's proceedings. The report also contains tool descriptions of the participating solvers.