La thèse s'intéresse à l'application et l'extension des méthodes SAT et SMT pour la biologie des systèmes. Plus particulièrement sont visées les problématiques issues de l'étude des réseaux métaboliques. L'état de l'art dans l'étude des réseaux métaboliques utilise de la programmation linéaire qui est extrêmement efficace pour lister toutes les solutions. Afin de pouvoir concurrencer la programmation linéaire nous nous orientons non pas vers l'énumération de toutes les voies mais vers l'énumération de voies satisfaisant des contraintes spécifiées par l'utilisateur. L'utilisation de SMT et les contraintes supplémentaires nous permettent d'utiliser des optimisations inaccessibles à la programmation linéaire. / The thesis focuses on the application and extension SAT and SMT methods for systems biology. In particular, will be targeted issues from the study of metabolic networks . The state of the art in the study of metabolic networks use linear programming that is extremely effective to list all the solutions. In order to compete with linear programming we do not try to list all pathway but enumerate pathway satisfying constraints specified by the user. The use of SMT and the additional constraints allow us to use inaccessible optimization for linear programming.

This thesis deals with the problematic of test-data generation for relational databases. The aim of the this thesis is to design and implement tool which meets defined constrains and allows us to generate test-data. This tool uses SMT solver for constraint solving and test-data generation.

L'analyse statique correcte d'un programme consiste à obtenir des propriétés vraies de toute exécution de ce programme. Celles-ci sont utiles pour démontrer des caractéristiques appréciables du logiciel, telles que l'absence de dépassement de capacité ou autre erreur à l'exécution quelle que soient les entrées du programme. Elles sont presque toujours établies à l'aide d'invariants inductifs : des propriétés vraies de l'état initial et telles que si elles sont vraies à une étape de calcul, alors elles restent vraies à l'étape suivante de la transition de calcul, donc sont toujours vraies par récurrence. L'interprétation abstraite est une approche traditionnelle de la recherche d'invariants numériques, que l'on peut exprimer comme une interprétation non-standard du programme dans un domaine abstrait choisi et ne tenant compte que de certaines propriétés intéressantes. Même dans un domaine aussi simple que les intervalles (un minorant et un majorant pour chaque variable), ce calcul ne converge pas nécessairement, et l'analyse doit recourir à des opérateurs d'élargissement pour forcer la convergence au détriment de la précision. Une autre approche, appelée itération de politique et inspirée par la théorie des jeux, garantit de trouver le plus fort invariant inductif dans le domaine abstrait choisi après un nombre fini d'itérations. Cependant, la description originale de cet algorithme souffrait de quelques faiblesses : elle se basait sur une conversion totale du programme en un système d'équations, sans intégration ni synergie avec les autres méthodes d'analyse. Notre nouvel algorithme est une forme locale de l'itération de politique, qui la replace dans l'itération de Kleene mais avec un opérateur d'élargissement spécial qui garantit d'obtenir le plus petit invariant inductif dans le domaine abstrait après un nombre fini de ses applications. L'itération de politique locale opère dans les domaines de contraintes linéaires données par patron, qui demandent de fixer d'avance la «forme» de l'invariant (p.ex. "x + 2y" pour obtenir "x + 2y <= 10" ). Notre seconde contribution théorique est le développement et la comparaison de plusieurs stratégies de synthèse de patrons, utilisées en conjonction avec l'itération locale de politiques. De plus, nous présentons une méthode pour générer des arbres d'accessibilité abstraite par interprétation abstraite, permettant la génération de traces de contre-exemples, et ensuite la génération de nouveaux patrons à partir d'interpolants de Craig. Notre troisième contribution concerne l'analyse interprocédurale de programmes, éventuellement récursifs. Nous proposons un algorithme qui génère pour chaque procédure un résumé, applicable à toute interprétation abstraite et notamment à l'itération de politique locale. Nous pouvons ainsi générer les invariants inductifs les plus forts dans le domaine pour un nombre fixé de résumés pour un programme récursif. Notre dernière contribution théorique est une méthode d'affaiblissement permettant de trouver des invariants inductifs, éventuellement disjonctifs, à partir de formules obtenues par exécution symbolique. Nous avons mis en œuvre toutes ces approches dans le système d'analyse statique CPAchecker, un logiciel libre, ce qui permet des communications et collaborations entre analyses. Nos techniques utilisent des résolveurs de satisfiabilité modulo théorie, capables, étant donné une formule de logique du premier ordre sur certaines théories, d'en donner un modèle ou de démontrer qu'aucun n'existe.Afin de simplifier les communications avec ces outils, nous présentons la bibliothèque JavaSMT, fournissant une interface générique. Cette bibliothèque a déjà démontré son utilité pour de nombreux chercheurs. / Static analysis concerns itself with deriving program properties which holduniversally for all program executions.Such properties are used for proving program properties (e.g. there neveroccurs an overflow or other runtime error regardless of a particular execution) and are almostinvariably established using inductive invariants: properties which holdfor the initial state and imply themselves under the program transition, and thushold universally due to induction.A traditional approach for finding numerical invariants is using abstractinterpretation, which can be seen as interpreting the program in the abstractdomain of choice, only tracking properties of interest.Yet even in the intervals abstract domain (upper and lower boundsfor each variable) such computation does not necessarily converge, and theanalysis has to resort to the use of widenings to enforceconvergence at the cost of precision.An alternative game-theoretic approach called policy iteration,guarantees to findthe least inductive invariant in the chosen abstract domain under the finitenumber of iterations.Yet the original description of the algorithm includes a number of drawbacks:it requires converting the entire program to an equation system,does not integrate with other approaches,and is unable to benefit from other analyses.Our new algorithm for running local policy iteration (LPI)instead formulates policy iteration as traditional Kleene iteration,with a widening operator that guarantees to return the least inductiveinvariant in the domain after finitely many applications.Local policy iteration runs in template linear constraint domains whichrequires setting in advance the ``shape'' of the derived invariant (e.g.$x + 2y$ for deriving $x + 2y leq 10$).Our second theoretical contribution involves development and comparison ofa number of different template synthesis strategies, when used in conjunctionwith LPI.Additionally, we present an approach for generating abstract reachabilitytrees using abstract interpretation,enabling the construction of counterexample traces,which in turns lets us generate new templates using Craig interpolants.In our third contribution we bring our attention to interprocedural andpotentially recursive programs.We develop an algorithm parameterizable with any abstract interpretation forsummary generation, and we study it's parameterization with LPI.The resulting approach is able to generate least inductive invariants in the domain for a fixed number of summaries for recursive programs.Our final theoretical contribution is a novel "formula slicing''method for finding potentially disjunctive inductive invariantsfrom program fragments obtained by symbolic execution.We implement all of these techniques in the open-source state-of-the-artCPAchecker program analysis framework, enabling communication and collaborationbetween different analyses.The techniques mentioned above rely onsatisfiability modulo theories solvers,which are capable ofgiving solutions tofirst-order formulas over certain theories or showingthat none exists.In order to simplify communication with such toolswe present the JavaSMT library, which provides a generic interface for suchcommunication.The library has shown itself to be a valuable tool, and is already used by manyresearchers.

Abstract SMT process is the most critical process to influence products quality in electronic assembly house process. Especially,the solder paste printing control is the key process to determine the yield rate of SMT quality. To own the capability to control quality of solder paste printing is the important thing what assembly house have to face it¡C For the purpose of gaining good SMT yield & solder paste printing stability ,the study use six sigma management technique & procedure (DMAIC--Define¡BMeasure¡BAnalyze¡BImprove & Control) make the main factors of solder paste printing¡Aincluding Printing speed¡BScraper pressure¡BStencil clean frequency¡Ato be the experiment factors of DOE(Design of Experiment)¡CThe DOE minimize the experiment number of times and provide a way of 2 levels factorial design combine RSM(Response Surface Methodology) experiment to get the optimization combination of factors¡¦ levels. Then evaluate how the optimization combination of factor levels to influence the quality of SMT¡C The study final found that there are a surprised & satisfied result on SMT yield improvement caused by optimization combination of factors¡¦ levels which 2 levels factorial design combine RSM experiment generated. It can provide the procedure & methodology for SMT assembly house reference to improve yield rate .

Due to the continued development of Internet technology, more and more people are willing to take advantage of high-interaction and diverse web applications to deal with commercial, knowledge-sharing, and social activities. However, while web applications deeply affect our society by degrees, hackers start exploiting web application vulnerabilities to attack innocent end user and back-end database, and therefore pose significant threat in information security. According to this situation, this paper proposes a detection mechanism based on Model Checking to detect web application vulnerabilities. We reduce the problem whether the vulnerabilities exist or not to a kind of SMT (Satisfiability Modulo Theories) problem, and analyze all of the traces of tainted data flow in web applications to find possible vulnerabilities by SMT solver. The experimental results show that the method we proposed can identify SQL injection and XSS vulnerabilities effectively, and prove our method is a feasible way to find web application vulnerabilities.

O avanço tecnológico no projeto de microprocessadores, nos recentes anos, tem seguido duas tendências principais. A primeira tenta aumentar a freqüência do relógio dos mesmos usando componentes digitais e técnicas VLSI mais eficientes. A segunda tenta explorar paralelismo no nível de instrução através da reorganização dos seus componentes internos. Dentro desta segunda abordagem estão as arquiteturas multi-tarefas simultâneas, que são capazes de extrair o paralelismo existente entre e dentro de diferentes tarefas das aplicações, executando instruções de vários fluxos simultaneamente e maximizando assim a utilização do hardware. Apesar do alto custo da implementação em hardware, acredita-se no potencial destas arquiteturas para o futuro próximo, pois é previsto que em breve haverá a disponibilidade de bilhões de transistores para o desenvolvimento de circuitos integrados. Assim, a questão principal a ser encarada talvez seja: como prover instruções paralelas para uma arquitetura deste tipo? Sabe-se que a maioria das aplicações é seqüencial pois os problemas nem sempre possuem uma solução paralela e quando a solução existe os programadores nem sempre têm habilidade para ver a solução paralela. Pensando nestas questões a arquitetura SEMPRE foi projetada. Esta arquitetura executa múltiplos processos, ao invés de múltiplas tarefas, aproveitando assim o paralelismo existente entre diferentes aplicações. Este paralelismo é mais expressivo do que aquele que existe entre tarefas dentro de uma mesma aplicação devido a não existência de sincronismo ou comunicação entre elas. Portanto, a arquitetura SEMPRE aproveita a grande quantidade de processos existentes nas estações de trabalho compartilhadas e servidores de rede. Além disso, esta arquitetura provê suporte de hardware para o escalonamento de processos e instruções especiais para o sistema operacional gerenciar processos com mínimo esforço. Assim, os tempos perdidos com o escalonamento de processos e as trocas de contextos são insignificantes nesta arquitetura, provendo ainda maior desempenho durante a execução das aplicações. Outra característica inovadora desta arquitetura é a existência de um mecanismo de prébusca de processos que, trabalhando em cooperação com o escalonamento de processos, permite reduzir faltas na cache de instruções. Também, devido a essa rápida troca de contexto, a arquitetura permite a definição de uma fatia de tempo (fatia de tempo) menor do que aquela praticada pelo sistema operacional, provendo maior dinâmica na execução das aplicações. A arquitetura SEMPRE foi analisada e avaliada usando modelagem analítica e simulação dirigida por execução de programas do SPEC95. A modelagem mostrou que o escalonamento por hardware reduz os efeitos colaterais causados pela presença de processos na cache de instruções e a simulação comprovou que as diferentes características desta arquitetura podem, juntas, prover ganho de desempenho razoável sobre outras arquiteturas multi-tarefas simultâneas equivalentes, com um pequeno acréscimo de hardware, melhor aproveitando as fatias de tempo atribuídas aos processos.

Many problems in nature can be represented as some kind of a satisfiability problem. Several SAT solvers and SMT solvers have been developed in the last decade with the goal of checking the satisfiability of different SAT problems. An all-solution satisfiability modulo theories on top of the Z3 SMT solver is presented that uses the clause blocking algorithm to find all the solution sets of a SAT problem. Then, an incremental All-SMT solver has been presented based on the all-SMT solver which is able to find the satisfiable answers of an incremental SMT problem based on the solution set of the original problem.

O avanço tecnológico no projeto de microprocessadores, nos recentes anos, tem seguido duas tendências principais. A primeira tenta aumentar a freqüência do relógio dos mesmos usando componentes digitais e técnicas VLSI mais eficientes. A segunda tenta explorar paralelismo no nível de instrução através da reorganização dos seus componentes internos. Dentro desta segunda abordagem estão as arquiteturas multi-tarefas simultâneas, que são capazes de extrair o paralelismo existente entre e dentro de diferentes tarefas das aplicações, executando instruções de vários fluxos simultaneamente e maximizando assim a utilização do hardware. Apesar do alto custo da implementação em hardware, acredita-se no potencial destas arquiteturas para o futuro próximo, pois é previsto que em breve haverá a disponibilidade de bilhões de transistores para o desenvolvimento de circuitos integrados. Assim, a questão principal a ser encarada talvez seja: como prover instruções paralelas para uma arquitetura deste tipo? Sabe-se que a maioria das aplicações é seqüencial pois os problemas nem sempre possuem uma solução paralela e quando a solução existe os programadores nem sempre têm habilidade para ver a solução paralela. Pensando nestas questões a arquitetura SEMPRE foi projetada. Esta arquitetura executa múltiplos processos, ao invés de múltiplas tarefas, aproveitando assim o paralelismo existente entre diferentes aplicações. Este paralelismo é mais expressivo do que aquele que existe entre tarefas dentro de uma mesma aplicação devido a não existência de sincronismo ou comunicação entre elas. Portanto, a arquitetura SEMPRE aproveita a grande quantidade de processos existentes nas estações de trabalho compartilhadas e servidores de rede. Além disso, esta arquitetura provê suporte de hardware para o escalonamento de processos e instruções especiais para o sistema operacional gerenciar processos com mínimo esforço. Assim, os tempos perdidos com o escalonamento de processos e as trocas de contextos são insignificantes nesta arquitetura, provendo ainda maior desempenho durante a execução das aplicações. Outra característica inovadora desta arquitetura é a existência de um mecanismo de prébusca de processos que, trabalhando em cooperação com o escalonamento de processos, permite reduzir faltas na cache de instruções. Também, devido a essa rápida troca de contexto, a arquitetura permite a definição de uma fatia de tempo (fatia de tempo) menor do que aquela praticada pelo sistema operacional, provendo maior dinâmica na execução das aplicações. A arquitetura SEMPRE foi analisada e avaliada usando modelagem analítica e simulação dirigida por execução de programas do SPEC95. A modelagem mostrou que o escalonamento por hardware reduz os efeitos colaterais causados pela presença de processos na cache de instruções e a simulação comprovou que as diferentes características desta arquitetura podem, juntas, prover ganho de desempenho razoável sobre outras arquiteturas multi-tarefas simultâneas equivalentes, com um pequeno acréscimo de hardware, melhor aproveitando as fatias de tempo atribuídas aos processos.

O avanço tecnológico no projeto de microprocessadores, nos recentes anos, tem seguido duas tendências principais. A primeira tenta aumentar a freqüência do relógio dos mesmos usando componentes digitais e técnicas VLSI mais eficientes. A segunda tenta explorar paralelismo no nível de instrução através da reorganização dos seus componentes internos. Dentro desta segunda abordagem estão as arquiteturas multi-tarefas simultâneas, que são capazes de extrair o paralelismo existente entre e dentro de diferentes tarefas das aplicações, executando instruções de vários fluxos simultaneamente e maximizando assim a utilização do hardware. Apesar do alto custo da implementação em hardware, acredita-se no potencial destas arquiteturas para o futuro próximo, pois é previsto que em breve haverá a disponibilidade de bilhões de transistores para o desenvolvimento de circuitos integrados. Assim, a questão principal a ser encarada talvez seja: como prover instruções paralelas para uma arquitetura deste tipo? Sabe-se que a maioria das aplicações é seqüencial pois os problemas nem sempre possuem uma solução paralela e quando a solução existe os programadores nem sempre têm habilidade para ver a solução paralela. Pensando nestas questões a arquitetura SEMPRE foi projetada. Esta arquitetura executa múltiplos processos, ao invés de múltiplas tarefas, aproveitando assim o paralelismo existente entre diferentes aplicações. Este paralelismo é mais expressivo do que aquele que existe entre tarefas dentro de uma mesma aplicação devido a não existência de sincronismo ou comunicação entre elas. Portanto, a arquitetura SEMPRE aproveita a grande quantidade de processos existentes nas estações de trabalho compartilhadas e servidores de rede. Além disso, esta arquitetura provê suporte de hardware para o escalonamento de processos e instruções especiais para o sistema operacional gerenciar processos com mínimo esforço. Assim, os tempos perdidos com o escalonamento de processos e as trocas de contextos são insignificantes nesta arquitetura, provendo ainda maior desempenho durante a execução das aplicações. Outra característica inovadora desta arquitetura é a existência de um mecanismo de prébusca de processos que, trabalhando em cooperação com o escalonamento de processos, permite reduzir faltas na cache de instruções. Também, devido a essa rápida troca de contexto, a arquitetura permite a definição de uma fatia de tempo (fatia de tempo) menor do que aquela praticada pelo sistema operacional, provendo maior dinâmica na execução das aplicações. A arquitetura SEMPRE foi analisada e avaliada usando modelagem analítica e simulação dirigida por execução de programas do SPEC95. A modelagem mostrou que o escalonamento por hardware reduz os efeitos colaterais causados pela presença de processos na cache de instruções e a simulação comprovou que as diferentes características desta arquitetura podem, juntas, prover ganho de desempenho razoável sobre outras arquiteturas multi-tarefas simultâneas equivalentes, com um pequeno acréscimo de hardware, melhor aproveitando as fatias de tempo atribuídas aos processos.

With the development of highly configurable and large software, a new challenge has to be addressed, when it comes to software testing. While traditional testing approaches might still apply and succeed in achieving a better quality of service, the high degree of customizable parts of such a system implies the mentioned testing activities on different configurations. If a formal notion is used to express the allowed configurations of a system, one might think of generating such configurations in an automated fashion. However, if there are constraints involved, traditional model-based test-case generation might cause problems to achieve a desired coherency. An idea is, to use those constraints to generate test-cases and to achieve coherency at the same time. Satisfiability modulo theories (SMT) has been an emerging field in current theoretical computer science and developed decision procedures to treat various theoretical fragments in a specific manner. The goal of this thesis is, to look at a translation mechanism from an expression language for constraints into SAT modulo theories and involve this technique into a test-case generation process. Furthermore, the balance between the generation of coherent test-cases as well as the problem-specific purposes of such test-cases is investigated.