Verification of tree-processing programs via higher-order model checking

DOI10.1017/S0960129513000054MaRDI QIDQ5740641zbMATH OpenOpenAlexFDO

Authors Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi

Publication date 27 July 2016

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0960129513000054

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Functional programming and lambda calculus (68N18)

Recommendations

• Automata-based abstraction for automated verification of higher-order tree-processing programs
• Model checking higher-order programs
• Verifying higher-order functions with tree automata
• Higher-order multi-parameter tree transducers and recursion schemes for program verification
• Types and higher-order recursion schemes for verification of higher-order programs

Cites work

• CDuce: an XML-centric general-purpose language
• Flow analysis of lazy higher-order functional programs
• High level tree transducers and iterated pushdown tree transducers
• Higher-order multi-parameter tree transducers and recursion schemes for program verification
• Macro tree transducers
• Regular expression types for XML
• Typechecking for XML transformers
• Verifying higher-order functional programs with pattern-matching algebraic data types
• XML Type Checking Using High-Level Tree Transducer

Cited in

(11)

• Automata-based verification of programs with tree updates
• Model checking higher-order programs
• Higher-order multi-parameter tree transducers and recursion schemes for program verification
• Verifying higher-order functional programs with pattern-matching algebraic data types
• Verifying higher-order functions with tree automata
• Automata-based abstraction for automated verification of higher-order tree-processing programs
• Types and higher-order recursion schemes for verification of higher-order programs
• Verified Operational Transformation for Trees
• Modular verification of higher-order functional programs
• Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
• Specifying and verifying higher-order Rust iterators

This page was built for publication: Verification of tree-processing programs via higher-order model checking

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