A traversal-based algorithm for higher-order model checking

DOI10.1145/2364527.2364578MaRDI QIDQ5168915zbMATH OpenOpenAlexFDO

Authors Robin P. Neatherway, S. J. Ramsay, Chih-Hao Luke Ong

Publication date 21 July 2014

Published in Proceedings of the 17th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2364527.2364578

zbMATH Keywords

higher-order programsmodel-checking

Mathematics Subject Classification ID

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

Recommendations

• Higher-order model checking: an overview
• Model checking higher-order programs
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.
• Practical alternating parity tree automata model checking of higher-order recursion schemes
• A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes

Cited in

(7)

• A ZDD-Based Efficient Higher-Order Model Checking Algorithm
• Practical alternating parity tree automata model checking of higher-order recursion schemes
• A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes
• Compositional higher-order model checking via -regular games over Böhm trees
• Higher-order model checking: an overview
• Streett Automata Model Checking of Higher-Order Recursion Schemes
• Higher-order model checking step by step

Describes a project that uses

Uses Software

• TravMC
• TRecS
• BLAST

This page was built for publication: A traversal-based algorithm for higher-order model checking

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