Higher-Order Model Checking: An Overview

DOI10.1109/LICS.2015.9zbMATH Open1401.68205OpenAlexW1525341697MaRDI QIDQ4635787FDOQ4635787

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)

Cited In (14)

• 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
• Higher-order program verification via HFL model checking
• 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
• 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?)
• Recent advances on reachability problems for valence systems (invited talk)
• 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)