Proceedings 5th Workshop on Horn Clauses for Verification and Synthesis

2018/09/12 by Temesghen Kahsai, German Vidal · 3 citations
Computer Science · #cs.LO #cs.PL #cs.SE

paper · pdf · doi:10.4204/eptcs.278

published as EPTCS 278, 2018

arxiv created 2018/09/12 · arxiv updated 2018/09/13

Abstract

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 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.

Cited by

• Bounded Symbolic Execution for Runtime Error Detection of Erlang Programs
• Towards Coinductive Theory Exploration in Horn Clause Logic: Position Paper
• A Simple Functional Presentation and an Inductive Correctness Proof of the Horn Algorithm
• Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions

Related

• Proceedings First Workshop on Horn Clauses for Verification and Synthesis
• Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis
• Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning
• Proceedings of the 12th Workshop on Horn Clauses for Verification and Synthesis
• Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis