Verifying higher-order functions with tree automata

DOI10.1007/978-3-319-89366-2_31MaRDI QIDQ1653017zbMATH OpenOpenAlexFDO

Authors Y. Aharonov

Publication date 17 July 2018

Copyright license Creative Commons Attribution 4.0 International

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

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)

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

Cited in

(14)

• Automating relatively complete verification of higher-order functional programs
• 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

Describes a project that uses

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)