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

Littérature citée [33 références]  Voir  Masquer  Télécharger
Contributeur : Timothée Haudebourg <>
Soumis le : lundi 23 octobre 2017 - 10:09:13
Dernière modification le : jeudi 11 janvier 2018 - 06:28:14


Verifying Higher-Order Functio...
Fichiers produits par l'(les) auteur(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〉



Consultations de la notice


Téléchargements de fichiers