SCD-Universite de Rennes 1 Automatic program verification by inference of relational models Vérification automatique de programmes par inférence de modèles relationnels Vérification formellePropriétés relationnellesDonnées algébriquesInférence de modèle Formal verificationRelational propertiesAlgebraic datatypesModel inference Programmation fonctionnelle (informatique) Approximation, Théorie de l' Vérification de modèles (informatique) Cette thèse porte sur la preuve automatique de propriétés concernant la relation entrée/sortie de programmes fonctionnels manipulant des types de données algébriques (ADT). De récents résultats montrent comment approximer un programme fonctionnel en utilisant un automate d'arbre. Bien qu'expressives, ces techniques ne peuvent pas prouver de propriété reliant l'entrée et la sortie d'une fonction, par exemple qu'inverser une liste préserve sa longueur. Dans cette thèse, nous nous appuyons sur ces résultats et définissons une procédure pour calculer ou sur-approximer une telle relation. Formellement, le problème de la vérification de programmes se réduit à la satisfiabilité de clauses, que nous résolvons en exhibant un modèle. Dans cette thèse, nous proposons deux représentations relationnelles de ces modèles de Herbrand : les automates d'arbres convolués et les shallow Horn clauses. Les automates d'arbres convolués généralisent les automates d'arbres et sont généralisés par les shallow Horn clauses. Le problème d'inférence du modèle de Herbrand découlant de la vérification relationnelle étant indécidable, nous proposons une procédure d'inférence incomplète mais correcte. Les expériences montrent que cette procédure est performante en pratique par rapport aux outils actuels, à la fois pour la vérification des propriétés et pour la recherche de contre-exemples. This thesis is concerned with automatically proving properties about the input/output relation of functional programs operating over algebraic data types. Recent results show how to approximate the image of a functional program using a regular tree language. Though expressive, those techniques cannot prove properties relating the input and the output of a function, e.g., proving that the output of a function reversing a list has the same length as the input list. In this thesis, we build upon those results and define a procedure to compute or over-approximate such a relation, thereby allowing to prove properties that require a more precise relational representation. Formally, the program verification problem reduces to satisfiability of clauses over the theory of algebraic data types, which we solve by exhibiting a Herbrand model of the clauses. In this thesis, we propose two relational representations of these Herbrand models: convoluted tree automata and shallow Horn clauses. Convoluted tree automata generalize tree automata and are in turn generalized by shallow Horn clauses. The Herbrand model inference problem arising from relational verification is undecidable, so we propose an incomplete but sound inference procedure. Experiments show that this procedure performs well in practice w.r.t. state of the art tools, both for verifying properties and for finding counterexamples. Electronic Thesis or DissertationText en application/pdf1 : 975 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/e5d2d3f1-3b72-43b9-8bba-25c7cd9c7f31 Losekoot Théo 1998-11-06 FR 284553107 tokoot@posteo.com 2024URENS102 http://www.theses.fr/2024URENS102 2024-12-17 Informatique Université de Rennesthesis.degree.grantor_1 26693823X Doctorat non ouiGenetThomasintervenant_1140601007JensenThomasintervenant_2059884959BaeldeDavidintervenant_3201647249GenetThomasintervenant_1140601007JensenThomasintervenant_2059884959TalbotJean-Marcintervenant_6103853294Kobayashi‎Naokiintervenant_4164909567SighireanuMihaelaintervenant_5 MATISSEecoleDoctorale_1 267602553 IRISA partenaireRecherche_1 026386909 ddc:004 GenetThomasJensenThomasBaeldeDavidKobayashi‎NaokiSighireanuMihaelaTalbotJean-MarcUniversité de RennesMATISSE IRISA ASCII PDF 998556