Schematic calculi for the analysis of decision procedures
Calculs schématiques pour l'analyse de procédures de décision
Résumé
In this thesis we address problems related to the verification of software-based systems. We are mostly interested in the (safe) design of decision procedures used in verification. In addition, we also consider a modularity problem for a modeling language used in the Why verification platform. Many verification problems can be reduced to a satisfiability problem modulo theories (SMT). In order to build satisfiability procedures Armando et al. have proposed in 2001 an approach based on rewriting. This approach uses a general calculus for equational reasoning named paramodulation. In general, a fair and exhaustive application of the rules of paramodulation calculus (PC) leads to a semi-decision procedure that halts on unsatisfiable inputs (the empty clause is then generated) but may diverge on satisfiable ones. Fortunately, it may also terminate for some theories of interest in verification, and thus it becomes a decision procedure. To reason on the paramodulation calculus, a schematic paramodulation calculus (SPC) has been studied, notably to automatically prove decidability of single theories and of their combinations. The advantage of SPC is that if it halts for one given abstract input, then PC halts for all the corresponding concrete inputs. More generally, SPC is an automated tool to check properties of PC like termination, stable infiniteness and deduction completeness. A major contribution of this thesis is a prototyping environment for designing and verifying decision procedures. This environment, based on the theoretical studies, is the first implementation of the schematic paramodulation calculus. It has been implemented from scratch on the firm basis provided by the Maude system based on rewriting logic. We show that this prototype is very useful to derive decidability and combinability of theories of practical interest in verification. It helps testing new saturation strategies and experimenting new extensions of the original (schematic) paramodulation calculus. This environment has been applied for the design of a schematic paramodulation calculus dedicated to the theory of Integer Offsets. This contribution is the first extension of the notion of schematic paramodulation to a built-in theory. This study has led to new automatic proof techniques that are different from those performed manually in the literature. The assumptions to apply our proof techniques are easy to satisfy for equational theories with counting operators. We illustrate our theoretical contribution on theories representing extensions of classical data structures such as lists and records. We have also addressed the problem of modular specification of generic Java classes and methods. We propose extensions to the Krakatoa Modeling Language, a part of the Why platform for proving that a Java or C program is a correct implementation of some specification. The key features are the introduction of parametricity both for types and for theories and an instantiation relation between theories. The proposed extensions are illustrated on two significant examples: the specification of the generic method for sorting arrays and for generic hash map. Both problems considered in this thesis are related to SMT solvers. Firstly, decision procedures are at the core of SMT solvers. Secondly, the Why platform extracts verification conditions from a source program annotated by specifications, and then transmits them to SMT solvers or proof assistants to check the program correctness.
Dans cette thèse, on étudie des problèmes liés à la vérification de systèmes (logiciels). On s'intéresse plus particulièrement à la conception sûre de procédures de décision utilisées en vérification. De plus, on considère également un problème de modularité pour un langage de modélisation utilisé dans la plateforme de vérification Why. De nombreux problèmes de vérification peuvent se réduire à un problème de satisfaisabilité modulo des théories (SMT). Pour construire des procédures de satisfaisabilité, Armando et al. ont proposé en 2001 une approche basée sur la réécriture. Cette approche utilise un calcul général pour le raisonnement équationnel appelé paramodulation. En général, une application équitable et exhaustive des règles du calcul de paramodulation (PC) conduit à une procédure de semi-décision qui termine sur les entrées insatisfaisables (la clause vide est alors engendrée), mais qui peut diverger sur les entrées satisfaisables. Mais ce calcul peut aussi terminer pour des théories intéressantes en vérification, et devient ainsi une procédure de décision. Pour raisonner sur ce calcul, un calcul de paramodulation schématique (SPC) a été étudié, en particulier pour prouver automatiquement la décidabilité de théories particulières et de leurs combinaisons. L'avantage de ce calcul SPC est que s'il termine sur une seule entrée abstraite, alors PC termine pour toutes les entrées concrètes correspondantes. Plus généralement, SPC est un outil automatique pour vérifier des propriétés de PC telles que la terminaison, la stable infinité et la complétude de déduction. Une contribution majeure de cette thèse est un environnement de prototypage pour la conception et la vérification de procédures de décision. Cet environnement, basé sur des fondements théoriques, est la première implantation du calcul de paramodulation schématique. Il a été complètement implanté sur la base solide fournie par le système Maude mettant en oeuvre la logique de réécriture. Nous montrons que ce prototype est très utile pour dériver la décidabilité et la combinabilité de théories intéressantes en pratique pour la vérification. Cet environnement est appliqué à la conception d'un calcul de paramodulation schématique dédié à une arithmétique de comptage. Cette contribution est la première extension de la notion de paramodulation schématique à une théorie prédéfinie. Cette étude a conduit à de nouvelles techniques de preuve automatique qui sont différentes de celles utilisées manuellement dans la littérature. Les hypothèses permettant d'appliquer nos techniques de preuves sont faciles à satisfaire pour les théories équationnelles avec opérateurs de comptage. Nous illustrons notre contribution théorique sur des théories représentant des extensions de structures de données classiques comme les listes ou les enregistrements. Nous avons également contribué au problème de la spécification modulaire pour les classes et méthodes Java génériques. Nous proposons des extensions du language de modélisation Krakatoa, faisant partie de la plateforme Why qui permet de prouver qu'un programme C ou Java est correct par rapport à sa spécification. Les caractéristiques essentielles de notre apport sont l'introduction de la paramétricité à la fois pour les types et les théories, ainsi qu'une relation d'instantiation entre les théories. Les extensions proposées sont illustrées sur deux exemples significatifs: tri de tableaux et fonctions de hachage. Les deux problèmes traités dans cette thèse ont pour point commun les solveurs SMT. Les procédures de décision sont les moteurs des solveurs SMT, alors que la plateforme Why engendre des conditions de vérification dérivées d'une programme source annoté, et les transmet aux solveurs SMT (ou assistants de preuve) pour vérfier la correction du programme.
Loading...