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 refinementintersection typeshigher-order model checking

Mathematics Subject Classification ID

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

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

(24)

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

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)