Fragments of arithmetic in a combination of decision procedures
Fragments de l'arithmétique dans une combinaison de procédures de décision
Résumé
Formal methods in software and hardware design often generate formulas that need to be validated, either interactively or automatically. Among the automatic tools, SMT (Satisfiability Modulo Theories) solvers are particularly suitable to discharge such proof obligations, since their input language is equational logic with symbols from various useful decidable fragments such as uninterpreted symbols, linear arithmetic, and usual data-structures like arrays or lists. In this thesis, we first present an approach to combine decision procedures and propositional solvers into an SMT-solver. This approach is based not only on the exchange of deducible equalities between decision procedures, but also on the generation of model-equalities by decision procedures. This extends nicely the classical Nelson-Oppen combination procedure in a simple platform to smoothly combine convex and non-convex theories. Secondly, we present an original algorithm for the arithmetic fragment of difference logic and the details of how to implement a decision procedure based on this algorithm. Difference logic is modeled using graph theory. The deductions and consistency checks performed by the algorithm are done by looking for negative cycles and calculating shortest paths incrementally. The last part of the thesis presents an original incremental variation of the simplex method that we use to build a decision procedure for linear arithmetic. As for difference logic, we present the details of the decision procedure that make it suitable for our combination framework used by SMT-solvers. The methods and techniques described in this thesis were implemented and are available in our open-source SMT-solver veriT.
Les méthodes formelles pour la conception des software et hardware génèrent souvent des formules qui doivent être validées, de manière interactive ou automatique. Parmi les outils automatiques, les solveurs SMT (Satisfiabilité Modulo Théories) sont particulièrement adaptés à la résolution de ces obligations de preuve, puisque leur langage d'entrée est la logique équationnelle avec des symboles provenant de divers fragments décidables utiles tels que les symboles non interprétés, l'arithmétique linéaire et des structures de données habituelles comme les tableaux ou les listes. Dans cette thèse, nous présentons une approche pour combiner des procédures de décision et des solveurs propositionnels dans un solveur SMT. Cette approche est fondée non seulement sur l'échange d'égalités déductibles entre les procédures de décision, mais aussi sur la génération d'égalités de modèle par des procédures de décision. Cela étend très bien la procédure classique de combinaison due à Nelson-Oppen dans une simple plate-forme pour combiner sans heurts des théories convexes et non convexes. Deuxièmement, nous présentons un algorithme original pour le fragment de l'arithmétique, appelé la logique de différence, et les détails sur la façon de mettre en oeuvre une procédure de décision basée sur cet algorithme. La logique de différence est modélisée en utilisant la théorie des graphes. Les déductions et les vérification de la cohérence effectués par l'algorithme se font par des recherches de cycles négatifs et des calculs de plus courts chemins de manière incrémentale. La dernière partie de la thèse présente une variation incrémentale originale de la méthode du simplexe que nous utilisons pour construire une procédure de décision pour l'arithmétique linéaire. Comme pour la logique de différence, nous présentons les détails de la procédure de décision qui la rend approprié pour notre plate-forme de combinaison utilisée par des solveurs SMT. Les méthodes et les techniques décrites dans cette thèse ont été mises en oeuvre et sont disponibles dans notre solveur SMT open-source, veriT.
Loading...