An overview of the HFL model checking project
From MaRDI portal
Publication:6647298
DOI10.4204/eptcs.344.1MaRDI QIDQ6647298
Publication date: 3 December 2024
Cites Work
- SMT-based model checking for recursive programs
- Results on the propositional \(\mu\)-calculus
- Predicate abstraction and CEGAR for disproving termination of higher-order functional programs
- Automata, logics, and infinite games. A guide to current research
- A new refinement type system for automated \(\nu\text{HFL}_\mathbb{Z}\) validity checking
- Removing algebraic data types from constrained Horn clauses using difference predicates
- Predicate abstraction and CEGAR for \(\nu \mathrm{HFL}_\mathbb{Z}\) validity checking
- Higher-order program verification via HFL model checking
- Temporal verification of higher-order functional programs
- Automating relatively complete verification of higher-order functional programs
- Horn Clause Solvers for Program Verification
- Saturation-Based Model Checking of Higher-Order Recursion Schemes.
- Proving that programs eventually do something good
- Solving Horn Clauses on Inductive Data Types Without Induction
- On Computability of Logical Approaches to Branching-Time Property Verification of Programs
- Fold/Unfold Transformations for Fixpoint Logic
- The Complexity of Model Checking Higher-Order Fixpoint Logic
- CONCUR 2004 - Concurrency Theory
- On the relationship between higher-order recursion schemes and higher-order fixpoint logic
- Model Checking Higher-Order Programs
- Automatic Termination Verification for Higher-Order Functional Programs
- Verification, Model Checking, and Abstract Interpretation
- ICE-based refinement type discovery for higher-order functional programs
- Constraint-based deductive model checking
- Syntax-guided termination analysis
- Temporal verification of programs via first-order fixpoint logic
- A type-based HFL model checking algorithm
This page was built for publication: An overview of the HFL model checking project
