Skip to Main content Skip to Navigation

Verifying Higher-Order Functions with Tree Automata: Extended Version

Thomas Genet 1 Timothée Haudebourg 1 Thomas Jensen 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : This paper describes a fully automatic technique for verifying properties of higher-order functional programs. Functional programs are modelled with term rewriting systems and tree automata are used to model reachable program states. From a tree automaton representing the initial state, it is possible to define a completion algorithm on tree automata for approximating the output set of the program to verify. We define a subclass of higher-order functional programs for which the completion is guaranteed to terminate. Furthermore, since precision of the completion is fixed by a set of equations, we also propose an algorithm to automatically generate sets of equations by iterative refinement. We present some experiments showing that the resulting verification technique is complementary and extends several state-of-the-art model-checking approaches for higher-order functional programs.
Document type :
Complete list of metadata

Cited literature [32 references]  Display  Hide  Download
Contributor : Timothée Haudebourg <>
Submitted on : Monday, October 23, 2017 - 10:09:13 AM
Last modification on : Thursday, January 7, 2021 - 4:12:18 PM
Long-term archiving on: : Wednesday, January 24, 2018 - 1:02:21 PM


Verifying Higher-Order Functio...
Files produced by the author(s)


  • HAL Id : hal-01614380, version 4


Thomas Genet, Timothée Haudebourg, Thomas Jensen. Verifying Higher-Order Functions with Tree Automata: Extended Version. [Technical Report] Irisa. 2017, pp.1-20. ⟨hal-01614380v4⟩



Record views


Files downloads