Higher-order model checking: an overview

DOI10.1109/LICS.2015.9MaRDI QIDQ4635787zbMATH OpenOpenAlexFDO

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

(28)

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

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)