A type-directed abstraction refinement approach to higher-order model checking

DOI10.1145/2535838.2535873zbMath1284.68414OpenAlexW2071164478MaRDI QIDQ5408403

Chih-Hao Luke Ong, Robin P. Neatherway, S. J. Ramsay

Publication date: 10 April 2014

Published in: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://research-information.bris.ac.uk/ws/files/135846861/popl216_ramsay.pdf

zbMATH Keywords

intersection typesabstraction refinementhigher-order model checking

Mathematics Subject Classification ID

Nonnumerical algorithms (68W05) Formal languages and automata (68Q45) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42)

Related Items (17)

Counterexample-guided partial bounding for recursive function synthesis ⋮ Higher-Order Model Checking in Direct Style ⋮ Recursion Schemes and the WMSO+U Logic ⋮ Horn Clause Solvers for Program Verification ⋮ Typing Weak MSOL Properties ⋮ Cost Automata, Safe Schemes, and Downward Closures ⋮ Unnamed Item ⋮ Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction Sequence ⋮ Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Automata, Logic and Games for the $$\lambda $$ -Calculus ⋮ Unnamed Item ⋮ Streett Automata Model Checking of Higher-Order Recursion Schemes ⋮ Unnamed Item ⋮ Local higher-order fixpoint iteration ⋮ The Complexity of the Diagonal Problem for Recursion Schemes

Uses Software

• C-SHORe

This page was built for publication: A type-directed abstraction refinement approach to higher-order model checking