Higher-order model checking: an overview
DOI10.1109/LICS.2015.9zbMATH Open1401.68205OpenAlexW1525341697MaRDI QIDQ4635787FDOQ4635787
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
Recommendations
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)
Cited In (27)
- Equivalence of pushdown automata via first-order grammars
- 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
- Model-checking higher-order programs with recursive types
- Practical alternating parity tree automata model checking of higher-order recursion schemes
- Tools and Algorithms for the Construction and Analysis of Systems
- Compositional higher-order model checking via \(\omega\)-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
- Title not available (Why is that?)
- General decidability results for asynchronous shared-memory programs: higher-order and beyond
- Model Checking Via ΓCFA
- 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
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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
- A bounded model checking technique for higher-order programs
- Higher-order model checking in direct style
- Mathematical Foundations of Computer Science 2005
- Epsilon-reducible context-free languages and characterizations of indexed languages
- Automata, Logic and Games for the $$\lambda $$ -Calculus
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)