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

DOI10.1145/2535838.2535873MaRDI QIDQ5408403zbMATH OpenOpenAlexFDO

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

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

abstraction refinementhigher-order model checkingintersection types

Mathematics Subject Classification ID

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

Recommendations

• An efficient approach for abstraction-refinement in model checking
• Abstraction and Refinement in Model Checking
• The abstraction-refinement framework in model checking
• Computer Aided Verification
• A satisfiability-based approach to abstraction refinement in model checking
• Making abstraction-refinement efficient in model checking
• Automated Technology for Verification and Analysis
• Higher-order model checking in direct style
• Refining and compressing abstract model checking

Cited in

(27)

• Equivalence-based abstraction refinement for HORS model checking
• Local higher-order fixpoint iteration
• Typestate verification: abstraction techniques and complexity results
• Horn clause solvers for program verification
• Almost every simply typed -term has a long -reduction sequence
• A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes
• Higher-order model checking in direct style
• Recursion schemes and the WMSO+U logic
• scientific article; zbMATH DE number 7029315 (Why is no real title available?)
• Parity to safety in polynomial time for pushdown and collapsible pushdown systems
• scientific article; zbMATH DE number 7455743 (Why is no real title available?)
• Intersection types for unboundedness problems
• Recursion schemes, the MSO logic, and the \textsf{U} quantifier
• Streett Automata Model Checking of Higher-Order Recursion Schemes
• On the termination problem for probabilistic higher-order recursive programs
• The Complexity of the Diagonal Problem for Recursion Schemes
• Automata, Logic and Games for the $$\lambda $$ -Calculus
• Programming Languages and Systems
• Model Checking Software
• Cost Automata, Safe Schemes, and Downward Closures
• A temporal logic for higher-order functional programs
• A type-based HFL model checking algorithm
• Partial bounding for recursive function synthesis
• Cost automata, safe schemes, and downward closures
• On average-case hardness of higher-order model checking
• Higher-order model checking step by step
• Counterexample-guided partial bounding for recursive function synthesis

Describes a project that uses

Uses Software

• C-SHORe

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

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