A type-directed abstraction refinement approach to higher-order model checking
DOI10.1145/2535838.2535873zbMATH Open1284.68414OpenAlexW2071164478MaRDI QIDQ5408403FDOQ5408403
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
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
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)
Cited In (24)
- 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 \(\mu \)HORS model checking
- Title not available (Why is that?)
- 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
- On the termination problem for probabilistic higher-order recursive programs
- Title not available (Why is that?)
- Horn clause solvers for program verification
- 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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Programming Languages and Systems
- Typestate verification: abstraction techniques and complexity results
- A temporal logic for higher-order functional programs
- A type-based HFL model checking algorithm
- Higher-order model checking in direct style
- Streett Automata Model Checking of Higher-Order Recursion Schemes
- Automata, Logic and Games for the $$\lambda $$ -Calculus
Uses Software
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)
