Higher-order model checking in direct style

DOI10.1007/978-3-319-47958-3_16MaRDI QIDQ3179299zbMATH OpenOpenAlexFDO

Authors Taku Terao, Takeshi Tsukada, Naoki Kobayashi

Publication date 21 December 2016

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-47958-3_16

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Model checking higher-order programs
• Higher-order model checking: an overview
• Model-checking higher-order programs with recursive types
• Higher-order program verification via HFL model checking
• A ZDD-Based Efficient Higher-Order Model Checking Algorithm

Cites work

• A type-directed abstraction refinement approach to higher-order model checking
• A ZDD-Based Efficient Higher-Order Model Checking Algorithm
• Abstracting abstract machines
• Automatic Termination Verification for Higher-Order Functional Programs
• C-SHORe: a collapsible approach to higher-order verification
• Complexity of model-checking call-by-value programs
• Higher-order model checking in direct style
• scientific article; zbMATH DE number 1324833 (Why is no real title available?)
• Model checking higher-order programs
• Pushdown control-flow analysis for free
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.
• Verifying higher-order functional programs with pattern-matching algebraic data types

Cited in

(16)

• Higher-order program verification via HFL model checking
• A ZDD-Based Efficient Higher-Order Model Checking Algorithm
• Model checking and functional program transformations
• Modular verification of higher-order functional programs
• Directed Model Checking for B: An Evaluation and New Techniques
• Higher-order model checking in direct style
• Higher-order model checking: an overview
• scientific article; zbMATH DE number 7297868 (Why is no real title available?)
• Model checking higher-order programs
• A type-directed abstraction refinement approach to higher-order model checking
• Verifying higher-order functional programs with pattern-matching algebraic data types
• Complexity of model-checking call-by-value programs
• Model Checking Via ΓCFA
• Verification, Model Checking, and Abstract Interpretation
• Model Checking Software
• A bounded model checking technique for higher-order programs

Describes a project that uses

Uses Software

• C-SHORe
• MoCHi

This page was built for publication: Higher-order model checking in direct style

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