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

program verificationhigher-order recursion schemehigher-order tree transducerstree-processing programs

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) 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

(15)

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

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)