An overview of the HFL model checking project
From MaRDI portal
Recommendations
Cites work
- A new refinement type system for automated \(\nu\text{HFL}_\mathbb{Z}\) validity checking
- A type-based HFL model checking algorithm
- Automata, logics, and infinite games. A guide to current research
- Automatic Termination Verification for Higher-Order Functional Programs
- Automating relatively complete verification of higher-order functional programs
- CONCUR 2004 - Concurrency Theory
- Constraint-based deductive model checking
- Fold/unfold transformations for fixpoint logic
- Higher-order program verification via HFL model checking
- Horn clause solvers for program verification
- ICE-based refinement type discovery for higher-order functional programs
- Model checking higher-order programs
- On Computability of Logical Approaches to Branching-Time Property Verification of Programs
- On the relationship between higher-order recursion schemes and higher-order fixpoint logic
- Predicate abstraction and CEGAR for \(\nu \mathrm{HFL}_\mathbb{Z}\) validity checking
- Predicate abstraction and CEGAR for disproving termination of higher-order functional programs
- Proving that programs eventually do something good
- Removing algebraic data types from constrained Horn clauses using difference predicates
- Results on the propositional \(\mu\)-calculus
- Saturation-Based Model Checking of Higher-Order Recursion Schemes.
- SMT-based model checking for recursive programs
- Solving Horn clauses on inductive data types without induction
- Syntax-guided termination analysis
- Temporal verification of higher-order functional programs
- Temporal verification of programs via first-order fixpoint logic
- The Complexity of Model Checking Higher-Order Fixpoint Logic
- Verification, Model Checking, and Abstract Interpretation
This page was built for publication: An overview of the HFL model checking project
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6647298)
