La vérification des programmes est un enjeu majeur pour les applications critiques comme l'aviation, l'aérospatiale ou les systèmes embarqués. Les approches Bounded model checking (e.g., CBMC) et de programmation par contraintes (e.g., CPBPV, …) reposent sur la recherche de contre-exemples qui violent une propriété du programme à vérifier. La recherche de tels contre-exemples peut être très longue et coûteuse lorsque les programmes à vérifier contiennent des calculs en virgule flottante. Ceci est dû en grande partie au fait que les stratégies de recherche existantes ont été conçues pour des domaines finis et, dans une moindre mesure, pour des domaines continus. Dans cette thèse, nous proposons un ensemble de stratégie de recherche dédié à la vérification de programme avec du calcul sur les flottants. Les stratégies proposées pour les choix de variables et de choix de valeur se basent sur des propriétés propres aux flottants. Ces propriétés utilisent des caractéristiques des domaines des variables, ou de la structure des contraintes. Certaines propriétés qui portent sur les domaines des variables sont classiques comme la taille et la cardinalité et d'autres beaucoup plus spécifiques comme la densité. Les notions de taille et cardinalité sont équivalentes sur les entiers, mais ne le sont pas sur les flottants. Ainsi la densité capture une variabilité qui est très spécifique aux flottants dont la moitié se trouve entre [-1,1]. De manière similaire les propriétés qui portent sur la structure des contraintes sont, pour certaines tels que le degré ou le nombre d’occurrences, issues des domaines finis, et pour d’autres beaucoup plus spécifiques, comme l’absorption, et la cancellation; ces deux propriétés capturent des phénomènes qui sont généralement la cause de fortes déviations du programme flottant vis-à-vis son interprétation sur les réels et donc de l’existence même de beaucoup de contre-exemples. Pour chaque propriété, deux stratégies de choix de variables sont proposées. La première choisit la variable qui minimise la propriété, alors que la seconde choisit la variable qui la maximise. Les stratégies de choix de valeurs essaient quant à elles de tirer profit des phénomènes d'absorption et de cancellation. L'évaluation de ces stratégies sur un ensemble de programmes réalistes est très encourageante : ces stratégies sont plus efficaces que les stratégies standards. / Program verification is a major issue for critical applications such as aviation, aerospace or embedded systems. Bounded model checking (e.g., CBMC) and constraint programming (e.g., CPBPV,...) approaches are based on the search for counter-examples that violate a property of the program to verify. The search for such counter-examples can be very time-consuming and costly when the programs to be verified contain floating point calculations. This is largely due to the fact that existing research strategies have been designed for finite domains and, to a lesser extent, for continuous domains. In this thesis, we propose a set of search strategies dedicated to program verification with floating point computation. The proposed strategies for variable and value selection are based on specific floating properties. These properties use characteristics of the variable domains, or the constraint structure. Some properties that focus on the domains of the variables are classic such as size and cardinality and others much more specific like density. The notions of size and cardinality are equivalent on the integers, but not on the floats. Density captures a variability that is very specific to the floats, half of which are between[-1.1]. Similarly, the properties that concern the structure of constraints are, for some such as the degree or number of occurrences, derived from finite domains, and for others much more specific, such as absorption, and cancellation; these two properties capture phenomena that are generally the cause of strong deviations of the floating point program from its interpretation on the reals and hence the existence of many counterexamples. For each property, two variable selection strategies are proposed. The first one chooses the variable that minimizes the property, while the second one chooses the variable that maximizes it. Value choice strategies try to take advantage of the phenomena of absorption and cancellation.

Plusieurs domaines d'application traitent des objets et des données complexes dont la structure et la sémantique de leurs composants sont des informations importantes pour leur manipulation et leur exploitation. La structure de graphe a été bien souvent adoptée, comme modèles de représentation, dans ces domaines. Elle permet de véhiculer un maximum d'informations, liées à la structure, la sémantique et au comportement de ces objets, nécessaires pour assurer une meilleure représentation et une manipulation efficace. Ainsi, lors d'une comparaison entre deux objets complexes, l'opération d'appariement est appliquée entre les graphes les modélisant. Nous nous sommes intéressés dans cette thèse à l'appariement approximatif qui permet de sélectionner les graphes les plus similaires au graphe d'une requête. L'objectif de notre travail est de contribuer à l'interrogation flexible et personnalisée d'objets complexes modélisés sous forme de graphes pour identifier les graphes les plus pertinents aux besoins de l'utilisateur, exprimés d'une manière partielle ou imprécise. Dans un premier temps, nous avons proposé un cadre de sélection de services Web modélisés sous forme de graphes qui permet (i) d'améliorer le processus d'appariement en intégrant les préférences des utilisateurs et l'aspect structurel des graphes comparés, et (ii) de retourner les services les plus pertinents. Une deuxième méthode d'évaluation de requêtes de recherche de graphes par similarité a également été présentée pour calculer le skyline de graphes d'une requête utilisateur en tenant compte de plusieurs mesures de distance de graphes. Enfin, des approches de raffinement ont été définies pour réduire la taille, souvent importante, du skyline. Elles ont pour but d'identifier et d'ordonner les points skyline qui répondent le mieux à la requête de l'utilisateur. / Several application domains deal with complex objects whose structure and semantics of their components are crucial for their handling. For this, graph structure has been adopted, as a model of representation, in these areas to capture a maximum of information, related to the structure, semantics and behavior of such objects, necessary for effective representation and processing. Thus, when comparing two complex objects, a matching technique is applied between their graph structures. In this thesis, we are interested in approximate matching techniques which constitute suitable tools to automatically find and select the most similar graphs to user graph query. The aim of our work is to develop methods to personalized and flexible querying of repositories of complex objects modeled thanks to graphs and then to return the graphs results that fit best the users ’needs, often expressed partially and in an imprecise way. In a first time, we propose a flexible approach for Web service retrieval that relies both on preference satisfiability and structural similarity between process model graphs. This approach allows (i) to improve the matching process by integrating user preferences and the graph structural aspect, and (ii) to return the most relevant services. A second method for evaluating graph similarity queries is also presented. It retrieves graph similarity skyline of a user query by considering a vector of several graph distance measures instead of a single measure. Thus, graphs which are maximally similar to graph query are returned in an ordered way. Finally, refinement methods have been developed to reduce the size of the skyline when it is of a significant size. They aim to identify and order skyline points that match best the user query.