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 :
Reports
[Technical Report] Irisa. 2017, pp.1-20
Liste complète des métadonnées

Cited literature [32 references]  Display  Hide  Download

https://hal.inria.fr/hal-01614380
Contributor : Timothée Haudebourg <>
Submitted on : Monday, October 23, 2017 - 10:09:13 AM
Last modification on : Wednesday, May 16, 2018 - 11:24:14 AM
Document(s) archivé(s) le : Wednesday, January 24, 2018 - 1:02:21 PM

File

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

Identifiers

  • HAL Id : hal-01614380, version 4

Citation

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〉

Share

Metrics

Record views

890

Files downloads

121