Compositional higher-order model checking via -regular games over Böhm trees

DOI10.1145/2603088.2603133MaRDI QIDQ4635663zbMATH OpenOpenAlexFDO

Authors

Publication date 23 April 2018

Published in Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (Search for Journal in Brave)

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

zbMATH Keywords

game semanticsintersection typehigher-order model checkingBöhm tree

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Games involving graphs (91A43) Semantics in the theory of computing (68Q55)

Recommendations

• Higher-order model checking: an overview
• Two-Level Game Semantics, Intersection Types, and Recursion Schemes
• Verification of Higher-Order Computation: A Game-Semantic Approach
• A traversal-based algorithm for higher-order model checking
• Model checking higher-order programs

Cited in

(5)

• Automata, Logic and Games for the $$\lambda $$ -Calculus
• On the termination problem for probabilistic higher-order recursive programs
• Compositional probabilistic model checking with string diagrams of MDPs
• Streett Automata Model Checking of Higher-Order Recursion Schemes
• A compositional approach to parity games

This page was built for publication: Compositional higher-order model checking via \(\omega\)-regular games over Böhm trees

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