Saturation-Based Model Checking of Higher-Order Recursion Schemes.

DOI10.4230/LIPIcs.CSL.2013.129zbMath1356.68141OpenAlexW2294925939MaRDI QIDQ2958519

Christopher H. Broadbent, Naoki Kobayashi

Publication date: 2 February 2017

Full work available at URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2013.129

zbMATH Keywords

model checkingintersection typeshigher-order recursion schemes

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Higher-Order Model Checking in Direct Style, Recursion Schemes and the WMSO+U Logic, 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, Unnamed Item, Domains for Higher-Order Games, 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