Verification of Higher-Order Computation: A Game-Semantic Approach

DOI10.1007/978-3-540-78739-6_23zbMATH Open1133.68379OpenAlexW2132220854MaRDI QIDQ5458405FDOQ5458405

Authors:

Publication date: 11 April 2008

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

Full work available at URL: https://doi.org/10.1007/978-3-540-78739-6_23

Recommendations

• scientific article; zbMATH DE number 5825969
• Recursion schemes, collapsible pushdown automata and higher-order model checking
• Model checking higher-order programs
• Some Results on a Game-Semantic Approach to Verifying Finitely-Presentable Infinite Structures (Extended Abstract)
• Types and higher-order recursion schemes for verification of higher-order programs

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Cited In (6)

• Some Results on a Game-Semantic Approach to Verifying Finitely-Presentable Infinite Structures (Extended Abstract)
• Domains for Higher-Order Games
• Compositional higher-order model checking via \(\omega\)-regular games over Böhm trees
• Recursion schemes, collapsible pushdown automata and higher-order model checking
• On Global Model Checking Trees Generated by Higher-Order Recursion Schemes
• State separation for code-based game-playing proofs

Uses Software

• Spec#
• Boogie

This page was built for publication: Verification of Higher-Order Computation: A Game-Semantic Approach

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