Le contrôle des accès concurrents à des données partagées et manipulées simultanément par plusieurs utilisateurs, ainsi que la reprise lors de pannes, sont des composantes essentielles de tout système de gestion de données actuel, notamment des bases de données. Nous mettons en évidence les limites inhérentes au critère le plus important du domaine : la commutativité des opérations sur les types de données abstraits. Ces limites nous confortent dans l'utilisation de techniques relativement simples dans les deux travaux ultérieurs. Ensuite, nous proposons une technique de contrôle de concurrence adaptée aux bases de données à objets car s'appuyant sur le graphe d'héritage. Cette proposition s'avère être une généralisation de la seule méthode implémentée : le protocole d'ORION. Combinant les limites théoriques de la commutativité à la notion de méthodes, qui encapsulent le comportement des objets, nous proposons une technique simple, et dans une large mesure suffisante, pour déterminer la commutativité entre méthodes. Cette dernière proposition combine les avantages de la technique précédente à ceux obtenus, involontairement, par la décomposition en première forme normale dans les bases de données relationnelles.

Le franchisage est un contrat qui est rarement équilibré. Il en est ainsi à cause d'une relation où l'on trouve une partie, généralement le franchiseur, qui domine le rapport contractuel. Cette relation économique et juridique appelle la plus grande attention en raison des investissements massifs qui y sont engagés. On verra souvent le franchisé assujetti à de nombreuses contraintes économiques, techniques et juridiques pratiquement exagérées sinon injustifiées. Cette situation n'est surtout pas sans solution. Cette étude s'efforce de trouver des remèdes aux problèmes posés par ce jeu de domination en examinant le contrat ainsi que ses différentes composantes. La méthode suivie consiste à examiner tout d'abord le concept relatif à chaque élément pris dans ce cadre contractuel précis tout en remontant à la définition de la franchise ainsi qu’à son objet, tout cela à la lumière de la notion d'équilibre et dans un souci de restaurer une certaine égalité de principe satisfaisant aux exigences de la justice contractuelle.Des définitions, des critères, des solutions, ainsi que des modifications y sont proposés à cette fin. / Franchising is a contract that is not always balanced. This is due to a relationship where one can find a party, usually the franchisor, dominating the contractual bond. The economic and legal relationships call for much more attention due to the massive investments involved. One will often notice the franchisee being subject to many economic, technical and legal constraints that are practically exaggerated if not unjustified. This is certainly not without any solution. This study attempts to find remedies to the problems raised by this game of domination through examining the contract as well as its various components. The followed method consists of, primarily, the examination of the concept behind each element in this precise contractual framework, to then go back to the definition of franchising, as well as its object; all in light of the concept of equilibrium in order to restore some equality of principle in accordance with the requirements of contractual justice.Definitions, criteria, solutions, and amendments are proposed to serve this purpose.

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.