As verification efforts using interactive theorem proving grow, we are in need of certified algorithms in computer algebra to tackle problems over the real numbers. This is important because uncertified procedures can drastically increase the size of the trust base and under- mine the overall confidence established by interactive theorem provers, which usually rely on a small kernel to ensure the soundness of derived results. This thesis describes an ongoing effort using the Isabelle theorem prover to certify the cylindrical algebraic decomposition (CAD) algorithm, which has been widely implemented to solve non-linear problems in various engineering and mathematical fields. Because of the sophistication of this algorithm, people are in doubt of the correctness of its implementation when deploying it to safety-critical verification projects, and such doubts motivate this thesis. In particular, this thesis proposes a library of real algebraic numbers, whose distinguishing features include a modular architecture and a sign determination algorithm requiring only rational arithmetic. With this library, an Isabelle tactic based on univariate CAD has been built in a certificate-based way: external, untrusted code delivers solutions in the form of certificates that are checked within Isabelle. To lay the foundation for the multivariate case, I have formalised various analytical results including Cauchy's residue theorem and the bivariate case of the projection theorem of CAD. During this process, I have also built a tactic to evaluate winding numbers through Cauchy indices and verified procedures to count complex roots in some domains. The formalisation effort in this thesis can be considered as the first step towards a certified computer algebra system inside a theorem prover, so that various engineering projections and mathematical calculations can be carried out in a high-confidence framework.

La vérification automatique est aujourd'hui devenue un domaine central de recherche en informatique. Depuis plus de 25 ans, une riche théorie a été développée menant à de nombreux outils, à la fois académiques et industriels, permettant la vérification de propriétés booléennes - celles qui peuvent être soit vraies soit fausses. Les besoins actuels évoluent vers une analyse plus fine, c'est-à-dire plus quantitative. L'extension des techniques de vérification aux domaines quantitatifs a débuté depuis 15 ans avec les systèmes probabilistes. Cependant, de nombreuses autres propriétés quantitatives existent, telles que la durée de vie d'un équipement, la consommation énergétique d'une application, la fiabilité d'un programme, ou le nombre de résultats d'une requête dans une base de données. Exprimer ces propriétés requiert de nouveaux langages de spécification, ainsi que des algorithmes vérifiant ces propriétés sur une structure donnée. Cette thèse a pour objectif l'étude de plusieurs formalismes permettant de spécifier de telles propriétés, qu'ils soient dénotationnels - expressions régulières, logiques monadiques ou logiques temporelles - ou davantage opérationnels, comme des automates pondérés, éventuellement étendus avec des jetons. Un premier objectif de ce manuscript est l'étude de résultats d'expressivité comparant ces formalismes. En particulier, on donne des traductions efficaces des formalismes dénotationnels vers celui opérationnel. Ces objets, ainsi que les résultats associés, sont présentés dans un cadre unifié de structures de graphes. Ils peuvent, entre autres, s'appliquer aux mots et arbres finis, aux mots emboîtés (nested words), aux images ou aux traces de Mazurkiewicz. Par conséquent, la vérification de propriétés quantitatives de traces de programmes (potentiellement récursifs, ou concurrents), les requêtes sur des documents XML (modélisant par exemple des bases de données), ou le traitement des langues naturelles sont des applications possibles. On s'intéresse ensuite aux questions algorithmiques que soulèvent naturellement ces résultats, tels que l'évaluation, la satisfaction et le model checking. En particulier, on étudie la décidabilité et la complexité de certains de ces problèmes, en fonction du semi-anneau sous-jacent et des structures considérées (mots, arbres...). Finalement, on considère des restrictions intéressantes des formalismes précédents. Certaines permettent d'étendre l'ensemble des semi-anneau sur lesquels on peut spécifier des propriétés quantitatives. Une autre est dédiée à l'étude du cas spécial de spécifications probabilistes : on étudie en particulier des fragments syntaxiques de nos formalismes génériques de spécification générant uniquement des comportements probabilistes. / Automatic verification has nowadays become a central domain of investigation in computer science. Over 25 years, a rich theory has been developed leading to numerous tools, both in academics and industry, allowing the verification of Boolean properties - those that can be either true or false. Current needs evolve to a finer analysis, a more quantitative one. Extension of verification techniques to quantitative domains has begun 15 years ago with probabilistic systems. However, many other quantitative properties are of interest, such as the lifespan of an equipment, energy consumption of an application, the reliability of a program, or the number of results matching a database query. Expressing these properties requires new specification languages, as well as algorithms checking these properties over a given structure. This thesis aims at investigating several formalisms, equipped with weights, able to specify such properties: denotational ones - like regular expressions, first-order logic with transitive closure, or temporal logics - or more operational ones, like navigating automata, possibly extended with pebbles. A first objective of this thesis is to study expressiveness results comparing these formalisms. In particular, we give efficient translations from denotational formalisms to the operational one. These objects, and the associated results, are presented in a unified framework of graph structures. This permits to handle finite words and trees, nested words, pictures or Mazurkiewicz traces, as special cases. Therefore, possible applications are the verification of quantitative properties of traces of programs (possibly recursive, or concurrent), querying of XML documents (modeling databases for example), or natural language processing. Second, we tackle some of the algorithmic questions that naturally arise in this context, like evaluation, satisfiability and model checking. In particular, we study some decidability and complexity results of these problems depending on the underlying semiring and the structures under consideration (words, trees...). Finally, we consider some interesting restrictions of the previous formalisms. Some permit to extend the class of semirings on which we may specify quantitative properties. Another is dedicated to the special case of probabilistic specifications: in particular, we study syntactic fragments of our generic specification formalisms generating only probabilistic behaviors.

Com a presença cada vez maior de sistemas computacionais e novas tecnologias no cotidiano das pessoas, garantir que eles não falhem e funcionem corretamente tornou-se algo de extrema importância. Além de indicar a qualidade do sistema, assegurar seu bom funcionamento é essencial para se evitar perdas, desde financeiras até de vidas. Uma das técnicas utilizadas para esta finalidade é a chamada verificação formal de programas. A partir da especificação do sistema, descrita numa linguagem formal, são definidas propriedades a serem satisfeitas e que certificariam a qualidade do software. Estas propriedades devem então ser implementadas para uso num verificador, que é a ferramenta responsável por executar a verificação e informar quais propriedades foram satisfeitas e quais não foram; no caso das propriedades terem sido violadas, o verificador deve indicar aos desenvolvedores os possíveis locais com código incorreto no sistema. A desvantagem do uso da verificação formal é, além do seu alto custo, a necessidade de haver pessoas com experiência em métodos formais para definir propriedades a partir da especificação formal do sistema, e convertê-las numa representação que possa ser entendida pelo verificador. Este processo de definição de propriedades é particularmente complexo, demorado e suscetível a erros, por ser feito em sua maior parte de forma manual. Para auxiliar os desenvolvedores na utilização da verificação formal em programas escritos em Java, propomos neste trabalho a geração de representação de propriedades para uso direto num verificador. As propriedades a serem geradas são objetivos de teste derivados da especificação formal do sistema. Estes objetivos de teste descrevem o comportamento esperado do sistema que deve ser observado durante sua execução. Ao estabelecer que o universo de propriedades corresponde ao universo de objetivos de teste do programa, garantimos que as propriedades geradas em nosso trabalho descrevem o comportamento esperado do programa por meio de caminhos de execução que levam a um estado de aceitação da propriedade, ou a um estado de violação. Assim, quando o verificador checa o objetivo de teste, ele consegue dar como resultado o veredicto de sucesso ou falha para a propriedade verificada, além de dados da cobertura dos caminhos de execução do programa que podem ser usados para análise do comportamento do programa que levou ao sucesso ou falha da propriedade verificada. / The task of guaranteeing that computational systems do not fail and work correctly has become extremely important with the growing presence of new technologies in people\'s lives. Therefore, it is essential to ensure that such systems work properly to confirm their high-quality and to avoid financial and even life losses. One of the techniques used to this purpose is called formal verification of programs. From the system specification, which should be described in a formal language, we define properties that must be satisfied during system execution to guarantee the software quality. Then, these properties are checked using a verifier, which is the tool responsible for running the verification and for notifying whether the property was satisfied by the program; if the property was violated, it indicates to software developers the possible location of faults in the system. The disadvantages of using formal verification are the high cost to apply this technique in practice, and the necessity of having people with experience in formal methods to derive the properties from system specification and define them in a formal representation that can be read by a program verifier. This particular task of deriving a property from system specification and defining it to be checked by a verifier is complex, time-consuming and error-prone, since it is usually done by hand. To help software developers in the application of formal verification in Java programs, we propose in this work the generation of properties formal representation for direct use in a verifier. The generated properties are test purposes, which are derived from system formal specification and present the desirable system behavior that must be observed during the system execution. Establishing that the universe of properties correspond to the universe of test purposes of a program, we guarantee that the generated properties describe the expected program behavior through execution traces that lead to either an accept state or a refuse state. Thus, when the verifier checks the test purpose, it can give a success/fail verdict for the property, and provide traces coverage data that can be used to analyze the program behavior that led to that verdict.

Les équipements intelligents, notamment les smartphones, sont la cible de nombreuses attaques de sécurité. Par ailleurs, la mise en œuvre de mécanismes de protection usuels est souvent inadaptée du fait de leurs ressources fortement contraintes. Dans ce contexte, nous proposons d'utiliser des chaînes de fonctions de sécurité qui sont composées de plusieurs services de sécurité, tels que des pare-feux ou des antivirus, automatiquement configurés et déployés dans le réseau. Cependant, ces chaînes sont connues pour être difficiles à valider. Cette difficulté est causée par la complexité de ces compositions qui impliquent des centaines, voire des milliers de règles de configuration. Dans cette thèse, nous proposons l'architecture d'un orchestrateur exploitant la programmabilité des réseaux pour automatiser la configuration et le déploiement de chaînes de fonctions de sécurité. Il est important que ces chaînes de sécurité soient correctes afin d’éviter l'introduction de failles de sécurité dans le réseau. Aussi, notre orchestrateur repose sur des méthodes automatiques de vérification et de synthèse, encore appelées méthodes formelles, pour assurer la correction des chaînes. Notre travail appréhende également l'optimisation du déploiement des chaînes dans le réseau, afin de préserver ses ressources et sa qualité de service. / Smart environments, in particular smartphones, are the target of multiple security attacks. Moreover, the deployment of traditional security mechanisms is often inadequate due to their highly constrained resources. In that context, we propose to use chains of security functions which are composed of several security services, such as firewalls or antivirus, automatically configured and deployed in the network. Chains of security functions are known as being error prone and hard to validate. This difficulty is caused by the complexity of these constructs that involve hundreds and even thousands of configuration rules. In this PhD thesis, we propose the architecture of an orchestrator, exploiting the programmability brought by software defined networking, for the automated configuration and deployment of chains of security functions. It is important to automatically insure that these security chains are correct, before their deployment in order to avoid the introduction of security breaches in the network. To do so, our orchestrator relies on methods of automated verification and synthesis, also known as formal methods, to ensure the correctness of the chains. Our work also consider the optimization of the deployment of chains of security functions in the network, in order to maintain its resources and quality of service.

Systems code is almost universally written in the C programming language or a variant. C has a very low level of type and memory abstraction and formal reasoning about C systems code requires a memory model that is able to capture the semantics of C pointers and types. At the same time, proof-based verification demands abstraction, in particular from the aliasing and frame problems. In this thesis, we study the mechanisation of a series of models, from semantic to separation logic, for achieving this abstraction when performing interactive theorem-prover based verification of C systems code in higher- order logic. We do not commit common oversimplifications, but correctly deal with C's model of programming language values and the heap, while developing the ability to reason abstractly and efficiently. We validate our work by demonstrating that the models are applicable to real, security- and safety-critical code by formally verifying the memory allocator of the L4 microkernel. All formalisations and proofs have been developed and machine-checked in the Isabelle/HOL theorem prover.

<p>Nowadays, embedded systems are becoming more and more complex. For this reason, designers focus more and more to adopt component-based methods for their designs. Consequently, there is an increasing interest on modeling and verification issues of component-based embedded systems. </p><p>In this thesis, a tool, which integrates modeling, simulation and verification of component-based embedded systems, is designed and implemented. This tool uses the PRES+, Petri Net based Representation for Embedded Systems, to model component-based embedded systems. Both simulation and verification of systems are based on the PRES+ models. </p><p>This tool consists of three integrated sub-tools, each of them with a graphical interface, the PRES+ Modeling tool, the PRES+ Simulation tool and the PRES+ Verification tool. The PRES+ Modeling tool is a graphical editor, with which system designers can model component-based embedded systems easily. The PRES+ Simulation tool, which is used to validate systems, visualizes the execution of a model in an intuitive manner. The PRES+ Verification tool provides a convenient access to a model checker, in which models can be formally verified with respect to temporal logic formulas.</p>

<p>The use of computer-based systems is rapidly increasing and such systems can now be found in a wide range of applications, including safety-critical applications such as cars and aircrafts. To make the development of such systems more efficient, there is a need for tools for automatic safety analysis, such as analysis of fault tolerance.</p><p>In this thesis, a tool for automatic formal analysis of fault tolerance was developed. The tool is built on top of the existing development environment for the synchronous language Esterel, and provides an output that can be visualised in the Item toolkit for fault tree analysis (FTA). The development of the tool demonstrates how fault tolerance analysis based on formal verification can be automated. The generated output from the fault tolerance analysis can be represented as a fault tree that is familiar to engineers from the traditional FTA analysis. The work also demonstrates that interesting attributes of the relationship between a critical fault combination and the input signals can be generated automatically.</p><p>Two case studies were used to test and demonstrate the functionality of the developed tool. A fault tolerance analysis was performed on a hydraulic leakage detection system, which is a real industrial system, but also on a synthetic system, which was modeled for this purpose.</p>

<p>Embedded systems are used in many technical products of today. The tendency also points to the fact that they are in many ways becoming more and more complex as technology advances. Systems like advanced avionics, air bags, ABS brakes or any real-time embedded system requires reliability, correctness and timeliness. This puts hard pressure on designers, analyzers and developers. The need for high performance and non failing systems has therefore led to a growing interest in modeling and verification of component-based embedded systems in order to reduce costs and simplify design and development. The solution proposed by the Embedded Systems Lab at Linköping University is the modeling language PRES+, Petri Net based Representation for Embedded Systems.</p><p>PRES+ models are then translated into timed automata, TA, which is used by the UPPAAL verification tool. To be able to verify timing properties the translated TA model must be instrumented with certain timers, called clocks. These clocks must be reset in a manner reflected by the property to be verified.</p><p>This thesis will provide a solution to the problem and also give the reader necessary information in order to understand the theoretical background needed. The thesis will also show the reader the importance of modeling and time verification in the development of embedded systems. A simple example is used to describe and visualize the benefit regarding real-time embedded systems as well as the importance of the ability to verify these systems.</p><p>The conclusion drawn stresses the fact that high development costs, possible gain of human lives and the problems in developing complex systems only emphasize the need for easy to handle and intuitive verification methods.</p>

Embedded systems are becoming increasingly common in our everyday lives. As technology progresses, these systems become more and more complex. Designers handle this increasing complexity by reusing existing components. At the same time, the systems must fulfill strict functional and non-functional requirements. This thesis presents novel and efficient techniques for the verification of component-based embedded system designs. As a common basis, these techniques have been developed using a Petri net based modelling approach, called PRES+. Two complementary problems are addressed: component verification and integration verification. With component verification the providers verify their components so that they function correctly if given inputs conforming to the assumptions imposed by the components on their environment. Two techniques for component verification are proposed in the thesis. The first technique enables formal verification of SystemC designs by translating them into the PRES+ representation. The second technique involves a simulation based approach into which formal methods are injected to boost verification efficiency. Provided that each individual component is verified and is guaranteed to function correctly, the components are interconnected to form a complete system. What remains to be verified is the interface logic, also called glue logic, and the interaction between components. Each glue logic and interface cannot be verified in isolation. It must be put into the context in which it is supposed to work. An appropriate environment must thus be derived from the components to which the glue logic is connected. This environment must capture the essential properties of the whole system with respect to the properties being verified. In this way, both the glue logic and the interaction of components through the glue logic are verified. The thesis presents algorithms for automatically creating such environments as well as the underlying theoretical framework and a step-by-step roadmap on how to apply these algorithms.

Today's EDA (Electronic Design Automation) industry faces enormous challenges. Their primary cause is the tremendous increase of the complexity of modern digital designs. Graph algorithms are widely applied to solve various EDA problems. In particular, graph dominators, which provide information about the origin and the end of reconverging paths in a circuit graph, proved to be useful in various CAD (Computer Aided Design) applications such as equivalence checking, ATPG, technology mapping, and power optimization. This thesis provides a study on graph dominators in logic synthesis and verification. The thesis contributes a set of algorithms for computing dominators in circuit graphs. An algorithm is proposed for finding absolute dominators in circuit graphs. The achieved speedup of three orders of magnitude on several designs enables the computation of absolute dominators in large industrial designs in a few seconds. Moreover, the computation of single-vertex dominators in large multiple-output circuit graphs is considerably improved. The proposed algorithm reduces the overall runtime by efficiently recognizing and re-using isomorphic structures in dominator trees rooted at different outputs of the circuit graph. Finally, common multiple-vertex dominators are introduced. The algorithm to compute them is faster and finds more multiple-vertex dominators than previous approaches. The thesis also proposes new dominator-based algorithms in the area of decomposition and combinational equivalence checking. A structural decomposition technique is introduced, which finds all simple-disjoint decompositions of a Boolean function which are reflected in the circuit graph. The experimental results demonstrate that the proposed technique outperforms state-of-the-art functional decomposition techniques. Finally, an approach to check the equivalence of two Boolean functions probabilistically is investigated. The proposed algorithm partitions the equivalence check employing dominators in the circuit graph. The experimental results confirm that, in comparison to traditional BDD-based equivalence checking methods, the memory consumption is considerably reduced by using the proposed technique. / QC 20100804