Predicate abstraction and CEGAR for HFL_Z validity checking

DOI10.1007/978-3-030-65474-0_7MaRDI QIDQ2233530zbMATH OpenOpenAlexFDO

Authors Naoki Iwayama, Naoki Kobayashi, Ryota Suzuki, Takeshi Tsukada

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) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A new refinement type system for automated \(\nu\text{HFL}_\mathbb{Z}\) validity checking
• Predicate abstraction and CEGAR for disproving termination of higher-order functional programs
• Verification of SpecC using predicate abstraction
• Predicate Abstraction in Program Verification: Survey and Current Trends
• Predicate abstraction for program verification
• A verified proof checker for higher-order logic
• Constructive consistency checking for partial specification in Z
• Computer Aided Verification
• scientific article; zbMATH DE number 2090118

Cites work

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

Cited in

(5)

• A new refinement type system for automated \(\nu\text{HFL}_\mathbb{Z}\) validity checking
• On higher-order reachability games vs may reachability
• Temporal verification of programs via first-order fixpoint logic
• An overview of the HFL model checking project
• On the relationship between Dijkstra monads and higher-order fixpoint logic

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233530)