Higher-order multi-parameter tree transducers and recursion schemes for program verification

DOI10.1145/1706299.1706355MaRDI QIDQ5255106zbMATH OpenOpenAlexFDO

Authors Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno

Publication date 11 June 2015

Published in Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1706299.1706355

zbMATH Keywords

higher-order recursion schemehigher-order tree transducersprogram verificationtree-processing programs

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verification of tree-processing programs via higher-order model checking
• Types and higher-order recursion schemes for verification of higher-order programs
• Model checking higher-order programs
• Verifying higher-order functions with tree automata
• Model checking and functional program transformations

Cited in

(17)

• Pattern eliminating transformations
• Backward type inference for XML queries
• Temporal refinements for guarded recursive types
• Verified Operational Transformation for Trees
• Reachability analysis of innermost rewriting
• Modular verification of higher-order functional programs
• scientific article; zbMATH DE number 5529981 (Why is no real title available?)
• scientific article; zbMATH DE number 7559409 (Why is no real title available?)
• Streett Automata Model Checking of Higher-Order Recursion Schemes
• Higher order symbolic execution for contract verification and refutation
• Verification of tree-processing programs via higher-order model checking
• Lifting numeric relational domains to algebraic data types
• Partial bounding for recursive function synthesis
• Infinitary refinement types for temporal properties in Scott domains
• An input-output relational domain for algebraic data types and functional arrays
• Termination criteria for tree automata completion
• Counterexample-guided partial bounding for recursive function synthesis

This page was built for publication: Higher-order multi-parameter tree transducers and recursion schemes for program verification

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