Higher-order model checking: an overview

DOI10.1109/LICS.2015.9MaRDI QIDQ4635787zbMATHOpenAlexFDO

Authors Luke Ong

Publication date 23 April 2018

Published in 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1109/lics.2015.9

zbMATH Keywords

model checkinglambda calculusprogram verificationfunctional programsrecursion schemes

Mathematics Subject Classification ID

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

Recommendations

• Model checking higher-order programs
• Higher-order model checking in direct style
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.
• Practical alternating parity tree automata model checking of higher-order recursion schemes
• A traversal-based algorithm for higher-order model checking

Cited in

(27)

• Deciding semantic finiteness of pushdown processes and first-order grammars w.r.t. bisimulation equivalence
• On the relationship between higher-order recursion schemes and higher-order fixpoint logic
• Relational semantics of linear logic and higher-order model checking
• A ZDD-Based Efficient Higher-Order Model Checking Algorithm
• Mathematical Foundations of Computer Science 2005
• Epsilon-reducible context-free languages and characterizations of indexed languages
• General decidability results for asynchronous shared-memory programs: higher-order and beyond
• Equivalence of pushdown automata via first-order grammars
• Compositional higher-order model checking via \(\omega\)-regular games over Böhm trees
• Model checking higher-order programs
• An overview of the HFL model checking project
• Reducing higher-order recursion scheme equivalence to coinductive higher-order constrained Horn clauses
• Higher-order model checking in direct style
• A bounded model checking technique for higher-order programs
• Model-checking higher-order programs with recursive types
• On Global Model Checking Trees Generated by Higher-Order Recursion Schemes
• scientific article; zbMATH DE number 7297868 (Why is no real title available?)
• Practical alternating parity tree automata model checking of higher-order recursion schemes
• Model Checking Via ΓCFA
• Higher-order program verification via HFL model checking
• Automata, Logic and Games for the $$\lambda $$ -Calculus
• General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
• scientific article; zbMATH DE number 7453200 (Why is no real title available?)
• Recent advances on reachability problems for valence systems (invited talk)
• A traversal-based algorithm for higher-order model checking
• Tools and Algorithms for the Construction and Analysis of Systems
• scientific article; zbMATH DE number 1852146 (Why is no real title available?)

This page was built for publication: Higher-order model checking: an overview

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