- 2024
- Temur Kutsia, Daniel Ventura, David Monniaux, José F. Morales:
Proceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis, LSFA/HCVS 2023, and 10th Workshop on Horn Clauses for Verification and SynthesisRome, Italy & Paris, France, 1-2 July, 2023 & 23rd April 2023. EPTCS 402, 2024 [contents] - 2023
- Laura P. Gamboa Guzman, Kristin Y. Rozier:
Stalnaker's Epistemic Logic in Isabelle/HOL. LSFA/HCVS 2023: 4-17 - Thaynara Arielly de Lima, Andréia Borges Avelar, André Luiz Galdino, Mauricio Ayala-Rincón:
Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms. LSFA/HCVS 2023: 18-33 - Alberto Momigliano, Martina Sassella:
More Church-Rosser Proofs in BELUGA. LSFA/HCVS 2023: 34-42 - Niccolò Veltri, Cheng-Syuan Wan
:
Semi-Substructural Logics with Additives. LSFA/HCVS 2023: 63-80 - Emanuele De Angelis, Hari Govind V. K.:
CHC-COMP 2023: Competition Report. LSFA/HCVS 2023: 83-104 - Daneshvar Amrollahi, Hossein Hojjat, Philipp Rümmer:
An Encoding for CLP Problems in SMT-LIB. LSFA/HCVS 2023: 118-130 - J. Tanner Slagel, Mariano M. Moscato, Lauren M. White, César A. Muñoz, Swee Balachandran, Aaron Dutle:
Embedding Differential Dynamic Logic in PVS. LSFA/HCVS 2023: 43-62 - Márk Somorjai, Mihály Dobos-Kovács, Zsófia Ádám, Levente Bajczi, András Vörös:
Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification. LSFA/HCVS 2023: 105-117 - 2022
- Robert Glück, Tetsuo Yokoyama:
Reversible Programming: A Case Study of Two String-Matching Algorithms. HCVS/VPT@ETAPS 2022: 1-13 - Bruno Blanchet:
The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm. HCVS/VPT@ETAPS 2022: 14-22 - Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti:
Contract Strengthening through Constrained Horn Clause Verification. HCVS/VPT@ETAPS 2022: 23-34 - Hossein Hojjat, Philipp Rümmer:
OptiRica: Towards an Efficient Optimizing Horn Solver. HCVS/VPT@ETAPS 2022: 35-43 - Emanuele De Angelis, Hari Govind V. K.:
CHC-COMP 2022: Competition Report. HCVS/VPT@ETAPS 2022: 44-62 - Geoffrey William Hamilton, Temesghen Kahsai, Maurizio Proietti:
Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation, HCVS/VPT@ETAPS 2022, and 10th International Workshop on Verification and Program TransformationMunich, Germany, 3rd April 2022. EPTCS 373, 2022 [contents] - 2021
- Naoki Kobayashi:
An Overview of the HFL Model Checking Project. HCVS@ETAPS 2021: 1-12 - Jesús J. Doménech, Samir Genaim:
Termination Analysis of Programs with Multiphase Control-Flow. HCVS@ETAPS 2021: 13-21 - Bishoksan Kafle, John P. Gallagher, Manuel V. Hermenegildo, Maximiliano Klemen, Pedro López-García, José F. Morales:
Regular Path Clauses and Their Application in Solving Loops. HCVS@ETAPS 2021: 22-35 - Jerome Jochems:
Reducing Higher-order Recursion Scheme Equivalence to Coinductive Higher-order Constrained Horn Clauses. HCVS@ETAPS 2021: 36-64 - Stefan Hetzl, Johannes Kloibhofer:
A Fixed-point Theorem for Horn Formula Equations. HCVS@ETAPS 2021: 65-78 - Brendan Hall, Sarat Chandra Varanasi, Jan Fiedor, Joaquín Arias, Kinjal Basu, Fang Li, Devesh Bhatt, Kevin Driscoll, Elmer Salazar, Gopal Gupta:
Knowledge-Assisted Reasoning of Model-Augmented System Requirements with Event Calculus and Goal-Directed Answer Set Programming. HCVS@ETAPS 2021: 79-90 - Grigory Fedyukovich, Philipp Rümmer:
Competition Report: CHC-COMP-21. HCVS@ETAPS 2021: 91-108 - Hossein Hojjat, Bishoksan Kafle:
Proceedings 8th Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS 2021, Virtual, 28th March 2021. EPTCS 344, 2021 [contents] - 2020
- Fabian Zaiser, C.-H. Luke Ong:
The Extended Theory of Trees and Algebraic (Co)datatypes. VPT/HCVS@ETAPS 2020: 167-196 - Alberto Pettorossi:
A Historical Account of My Early Research Interests. VPT/HCVS@ETAPS 2020: 1-28 - Alain Finkel:
From Well Structured Transition Systems to Program Verification. VPT/HCVS@ETAPS 2020: 44-49 - John P. Gallagher, Manuel V. Hermenegildo, Bishoksan Kafle, Maximiliano Klemen, Pedro López-García, José F. Morales:
From Big-Step to Small-Step Semantics and Back with Interpreter Specialisation. VPT/HCVS@ETAPS 2020: 50-64 - Neil D. Jones, Siddharth Bhaskar, Cynthia Kop, Jakob Grue Simonsen:
Cons-free Programs and Complexity Classes between LOGSPACE and PTIME. VPT/HCVS@ETAPS 2020: 65-79 - Michael Leuschel:
Prolog for Verification, Analysis and Transformation Tools. VPT/HCVS@ETAPS 2020: 80-94 - Emanuele De Angelis, Fabio Fioravanti, Maurizio Proietti:
Transformational Verification of Quicksort. VPT/HCVS@ETAPS 2020: 95-109
