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

DOI10.1017/S0960129513000054zbMATH Open1361.68152OpenAlexW2002702549MaRDI QIDQ5740641FDOQ5740641

Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno

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

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

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)

Cites Work

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

Cited In (3)

• Automata-based verification of programs with tree updates
• Verified Operational Transformation for Trees
• Abstract Regular Tree Model Checking of Complex Dynamic Data Structures

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)