Comme les syst`emes mat´eriels et logiciels grandissent de fa¸con continue en ´echelle et fonctionnalit´es, la probabilit´e d’erreurs subtiles de- vient toujours plus grande. Les techniques d’abstraction, souvent bas´ees sur l’interpr´etation abstraite de Cousot, fournissent une m´ethode pour ex´ecuter symboliquement les syst`emes en utilisant le domaine abstrait `a la place du domaine concret. Dans cette th`ese, on introduit des techniques d’abstraction pour les logiques sous des interpr´etations multi-valu´ees. Beaucoup d’applications des logiques multi-valu´ees ont ´et´e trouv´ees dans la v´erification du mat´eriel et du logiciel. Pour la v´erification du mat´eriel, des outils de simulation et des r´ealisations des circuits multi-valu´es v´eritables ont ´et´e propos´es, les risques dynamiques ont ´et´e model´es en introduisant des ´etats faux pour trouver des r´egions chevauchantes des signaux en concurrence, etc. Pour la v´erification du logiciel on a besoin d’incertitude parce qu’on ne peut savoir si certains comportements devraient ˆetre possibles et on a besoin du d´esaccord parce que l’on peut avoir des acteurs diff´erents qui sont en d´esaccord pour la mani`ere dont les syst`emes devraient se comporter. Les abstractions sont obtenues en appliquant des relations d’´equivalence et apr`es, les symboles pr´edicatifs de la logique sont red´efinis `a s’appliquer cor- rectement aux classes d’´equivalence `a l’aide des politiques d’interpr´etation. On fournit des r´esultats de pr´eservation pour la logique de premier ordre, pour la logique temporelle et pour la logique temporelle de la connaissance. Avant de discuter les abstractions multi-valu´ees pour la logique temporelle, nous pr´esentons une ´etude de cas pour utiliser l’abstraction dans le contexte des mod`eles du contrˆole d’acc`es. Nous fournirons aussi une technique d’abstraction pour les types de do- nn´ees. Cette technique d’abstraction peut ˆetre ´elargie pour les types abstraits de donn´ees. Ici, les abstractions sont appliqu´ees aux sp´ecifications initiales au moyen des ´equations et ils sont appel´es des abstractions ´equationnelles. De plus, la technique d’abstraction pr´esent´ee g´en´eralise et clarifie la nature de beaucoup de techniques d’abstraction trouv´ees dans la litt´erature, telles: la technique de dupliquer les symboles pr´edicatifs, shape analysis, l’abstraction par pr´edicats, l’approche de McMillan, etc. Pour raisonner au sujet des syst`emes dynamiques, on introduit les types de donn´ees dynamiques et on ´etend la m´ethode d’abstraction ant´erieure `a ce cas. Le probl`eme principal qui survient quand on utilise les abstractions est de trouver l’abstraction convenable ou de raffiner une abstraction d´ej`a existante pour en obtenir une meilleure. On prouve que les techniques d’abstraction que nous avons introduites pour les types de donn´ees sous l’interpr´etation 3- valu´ee Kleene, peuvent ˆetre utilis´ees dans une proc´edure de raffinement. De plus, on montre que la proc´edure de raffinement guid´e par contre-exemple est plus efficace quand on l’utilise sous les abstractions ´equationnelles / As the hardware and software systems are growing continuously in scale and functionality, the likelihood of subtle errors becomes greater. Abstraction techniques, often based on abstract interpretation, provide a method for symbolically executing systems using the abstract instead of the concrete domain. In this thesis, we are concerned with abstractions for logics under multi-valued interpretations. Many applications of multi-valued logics have been found in hardware and software verification. For hardware verification, simulation tools and imple- mentations of genuinely multi-valued circuits have been proposed, dynamic hazards have been modeled by introducing pseudo states to find overlapping regions of competing signals, implementation of gates have been verified on the basis of switch level models, etc. For software verification, we need uncer- tainty because we may not know whether some behaviors should be possible, we need disagreement because we may have different stakeholders that dis- agree about how the systems should behave and we need to represent relative importance because some behaviors are essential and others may or may not be implemented. The abstractions are obtained by applying equivalence relations and then, the predicate symbols of the logic are re-defined to work properly on equiva- lence classes by using interpretation policies. We provide preservation results for first-order logic, temporal logic, and temporal logic of knowledge. As a case study, we show how abstraction can be used to solve the safety problem for protection systems which model access control policies. The use of abstraction in the context of data types, is also investigated. This technique scales well from data types to abstract data types. Here, abstractions are applied to initial specifications by means of equations and they are called equationally specified abstractions. Moreover, the abstraction technique we propose generalizes and clarifies the nature of many abstraction techniques found in the literature, such as the technique of duplicating pred- icate symbols, shape analysis, predicate abstraction, McMillan’s approach, etc. To reason about dynamic systems, we introduce dynamic data types and extend the previous abstraction technique to this case. The main problem that arises when using abstraction techniques is to find the suitable abstraction or to refine an already existing abstraction in order to obtain a better one. In this thesis, we prove that the abstraction techniques for data types, under Kleene’s three-valued interpretation, can be used in a refinement procedure. Moreover, we show that the counterexample guided abstraction refinement procedure (CEGAR) works better when used with equationally specified abstractions

Comme les systèmes matériels et logiciels grandissent de façon continue en échelle et fonctionnalités, la probabilité d'erreurs subtiles de- vient toujours plus grande. Les techniques d'abstraction, souvent basées sur l'interprétation abstraite de Cousot, fournissent une méthode pour exécuter symboliquement les systèmes en utilisant le domaine abstrait 'a la place du domaine concret. Dans cette thèse, on introduit des techniques d'abstraction pour les logiques sous des interprétations multivaluées. Beaucoup d'applications des logiques multivaluées ont été trouvées dans la vérification du matériel et du logiciel. Pour la vérification du matériel, des outils de simulation et des réalisations des circuits multivaluées véritables ont été proposés, les risques dynamiques ont été modelés en introduisant des 'états faux pour trouver des régions chevauchantes des signaux en concurrence, etc. Pour la vérification du logiciel on a besoin d'incertitude parce qu'on ne peut savoir si certains comportements devraient être possibles et on a besoin du désaccord parce que l'on peut avoir des acteurs différents qui sont en désaccord pour la manière dont les systèmes devraient se comporter. Les abstractions sont obtenues en appliquant des relations d''équivalence et après, les symboles prédicatifs de la logique sont redéfinis 'a s'appliquer cor- correctement aux classes d''équivalence 'a l'aide des politiques d'interprétation. On fournit des résultats de préservation pour la logique de premier ordre, pour la logique temporelle et pour la logique temporelle de la connaissance. Avant de discuter les abstractions multivaluées pour la logique temporelle, nous présentons une 'étude de cas pour utiliser l'abstraction dans le contexte des modèles du contrôle d'accès. Nous fournirons aussi une technique d'abstraction pour les types de données. Cette technique d'abstraction peut être 'élargie pour les types abstraits de données. Ici, les abstractions sont appliquées aux spécifications initiales au moyen des 'équations et ils sont appelés des abstractions 'équationnelles. De plus, la technique d'abstraction présentée généralise et clarifie la nature de beaucoup de techniques d'abstraction trouvées dans la littérature, telles: la technique de dupliquer les symboles prédicatifs, shape analysis, l'abstraction par prédicats, l'approche de McMillan, etc. Pour raisonner au sujet des systèmes dynamiques, on introduit les types de données dynamiques et on étend la méthode d'abstraction antérieure 'a ce cas. Le problème principal qui survient quand on utilise les abstractions est de trouver l'abstraction convenable ou de raffiner une abstraction déjà existante pour en obtenir une meilleure. On prouve que les techniques d'abstraction que nous avons introduites pour les types de données sous interprétation 3- valu'ee Kleene, peuvent être utilisées dans une procédure de raffinement. De plus, on montre que la procédure de raffinement guide par contre-exemple est plus efficace quand on l'utilise sous les abstractions 'équationnelles.

L'essence de cette thèse est de produire des théorèmes de représentation et d'impossibilité pour des familles de relations de conséquence et d'opérateurs de révision. Dans un premier temps, on s'intéressera à des relations de conséquence préférentielles (au sens de Kraus, Lehmann et Magidor) et pivotantes (au sens de Makinson). Ce sont des relations plausibles (les premières ne sont pas monotones, les secondes si) conçues pour traiter des informations incomplètes. On les étudiera dans des cadres paraconsistants tels que celui de la logique de Belnap, ce qui les rendra aussi utiles pour traiter des informations incohérentes. En seconde partie, on s'intéressera à une approche à la révision des croyances introduite par Lehmann, Magidor et Schlechta. Elle est basée sur des distances entre interprétations et présente l'avantage de définir des opérateurs de révision qui se comportent bien en cas d'itération.