Spelling suggestions: "subject:"arithmétique linéaire"" "subject:"arithmétique inéaire""
1 |
Fragments de l'arithmétique dans une combinaison de procédures de décisionCaminha Barbosa De Oliveira, Diego 14 March 2011 (has links) (PDF)
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.
|
2 |
Strengthening the heart of an SMT-solver : Design and implementation of efficient decision procedures / Renforcement du noyau d’un démonstrateur SMT : Conception et implantation de procédures de décisions efficacesIguernelala, Mohamed 10 June 2013 (has links)
Cette thèse s'intéresse à la démonstration automatique de la validité de formules mathématiques issues de la preuve de programmes. Elle se focalise tout particulièrement sur la Satisfiabilité Modulo Théories (SMT): un jeune domaine de recherche qui a connu de grands progrès durant la dernière décennie. Les démonstrateurs de cette famille ont des applications diverses dans la conception de microprocesseurs, la preuve de programmes, le model-checking, etc.Les démonstrateurs SMT offrent un bon compromis entre l'expressivité et l'efficacité. Ils reposent sur une coopération étroite d'un solveur SAT avec une combinaison de procédures de décision pour des théories spécifiques comme la théorie de l'égalité libre avec des symboles non interprétés, l'arithmétique linéaire sur les entiers et les rationnels, et la théorie des tableaux.L'objectif de cette thèse est d'améliorer l'efficacité et l'expressivité du démonstrateur SMT Alt-Ergo. Pour cela, nous proposons une nouvelle procédure de décision pour la théorie de l'arithmétique linéaire sur les entiers. Cette procédure est inspirée par la méthode de Fourier-Motzkin, mais elle utilise un simplexe sur les rationnels pour effectuer les calculs en pratique. Nous proposons également un nouveau mécanisme de combinaison, capable de raisonner dans l'union de la théorie de l'égalité libre, la théorie AC des symboles associatifs et commutatifs et une théorie arbitraire deShostak. Ce mécanisme est une extension modulaire et non intrusive de la procédure de completion close modulo AC avec la théorie de Shostak. Aussi, nous avons étendu Alt-Ergo avec des procédures de décision existantes pour y intégrer d'autres théories intéressantes comme la théorie de types de données énumérés et la théorie des tableaux. Enfin, nous avons exploré des techniques de simplification de formules en amont et l'amélioration de son solveur SAT. / This thesis tackles the problem of automatically proving the validity of mathematical formulas generated by program verification tools. In particular, it focuses on Satisfiability Modulo Theories (SMT): a young research topic that has seen great advances during the last decade. The solvers of this family have various applications in hardware design, program verification, model checking, etc.SMT solvers offer a good compromise between expressiveness and efficiency. They rely on a tight cooperation between a SAT solver and a combination of decision procedures for specific theories, such as the free theory of equality with uninterpreted symbols, linear arithmetic over integers and rationals, or the theory of arrays.This thesis aims at improving the efficiency and the expressiveness of the Alt-Ergo SMT solver. For that, we designed a new decision procedure for the theory of linear integer arithmetic. This procedure is inspired by Fourier-Motzkin's method, but it uses a rational simplex to perform computations in practice. We have also designed a new combination framework, capable of reasoning in the union of the free theory of equality, the AC theory of associative and commutativesymbols, and an arbitrary signature-disjoint Shostak theory. This framework is a modular and non-intrusive extension of the ground AC completion procedure with the given Shostak theory. In addition, we have extended Alt-Ergo with existing decision procedures to integrate additional interesting theories, such as the theory of enumerated data types and the theory of arrays. Finally, we have explored preprocessing techniques for formulas simplification as well as the enhancement of Alt-Ergo's SAT solver.
|
Page generated in 0.0332 seconds