A ZDD-Based Efficient Higher-Order Model Checking Algorithm

DOI10.1007/978-3-319-12736-1_19MaRDI QIDQ2789057zbMATH OpenOpenAlexFDO

Authors Taku Terao, Naoki Kobayashi

Publication date 26 February 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-12736-1_19

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A traversal-based algorithm for higher-order model checking
• Higher-order model checking: an overview
• Higher-order model checking in direct style
• Mathematical Foundations of Computer Science 2005
• The Complexity of Model Checking Higher-Order Fixpoint Logic
• Model-checking CSP-Z: Strategy, tool support and industrial application
• Model checking higher-order programs
• scientific article; zbMATH DE number 1670780

Cited in

(9)

• A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes
• Parity to safety in polynomial time for pushdown and collapsible pushdown systems
• A type-directed negation elimination
• ZB 2005: Formal Specification and Development in Z and B
• A Z approach in validating ORA-SS data models
• Higher-order model checking in direct style
• A bounded model checking technique for higher-order programs
• Streett Automata Model Checking of Higher-Order Recursion Schemes
• C-SHORe: a collapsible approach to higher-order verification

This page was built for publication: A ZDD-Based Efficient Higher-Order Model Checking Algorithm

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