Verifying higher-order functions with tree automata

DOI10.1007/978-3-319-89366-2_31zbMATH Open1504.68129OpenAlexW2767047126MaRDI QIDQ1653017FDOQ1653017

Authors: Y. Aharonov 

Publication date: 17 July 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-89366-2_31

Recommendations

• Automata-based abstraction for automated verification of higher-order tree-processing programs
• Automating relatively complete verification of higher-order functional programs
• Verification of tree-processing programs via higher-order model checking
• Automatic Termination Verification for Higher-Order Functional Programs
• Model checking higher-order programs

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Functional programming and lambda calculus (68N18)

Cited In (14)

• Pattern eliminating transformations
• Automata-based verification of programs with tree updates
• Lifting numeric relational domains to algebraic data types
• Towards static analysis of functional programs using tree automata completion
• Higher-order multi-parameter tree transducers and recursion schemes for program verification
• Temporal verification of higher-order functional programs
• Automata-based abstraction for automated verification of higher-order tree-processing programs
• Verification of tree-processing programs via higher-order model checking
• Certifying a Tree Automata Completion Checker
• Modular verification of higher-order functional programs
• Executing and verifying higher-order functional-imperative programs in Maude
• SAT-based automated completion for reachability analysis
• Specifying and verifying higher-order Rust iterators
• Automating relatively complete verification of higher-order functional programs

Uses Software

• Coq

This page was built for publication: Verifying higher-order functions with tree automata

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