Predicate abstraction and CEGAR for \(\nu \mathrm{HFL}_\mathbb{Z}\) validity checking

DOI10.1007/978-3-030-65474-0_7zbMath1474.68190OpenAlexW3120672074MaRDI QIDQ2233530

Naoki Iwayama, Takeshi Tsukada, Ryota Suzuki, Naoki Kobayashi

Publication date: 18 October 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-65474-0_7

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

On higher-order reachability games vs may reachability

Cites Work

• Predicate abstraction and CEGAR for disproving termination of higher-order functional programs
• Higher-order program verification via HFL model checking
• Compositional and Lightweight Dependent Type Inference for ML
• Learning refinement types
• Dependent types from counterexamples
• CONCUR 2004 - Concurrency Theory
• On the relationship between higher-order recursion schemes and higher-order fixpoint logic
• ICE-based refinement type discovery for higher-order functional programs

This page was built for publication: Predicate abstraction and CEGAR for \(\nu \mathrm{HFL}_\mathbb{Z}\) validity checking