Behavioral synthesis is the process of compiling an Electronic System Level (ESL) design to a register-transfer level (RTL) implementation. ESL specifications define the design functionality at a high level of abstraction (e.g., with C/C++ or SystemC), and thus provide a promising approach to address the exacting demands to develop feature-rich, optimized, and complex hardware systems within aggressive time-to-market schedules. Behavioral synthesis entails application of complex and error-prone transformations during the compilation process. Therefore, the adoption of behavioral synthesis highly depends on our ability to ensure that the synthesized RTL conforms to the ESL description. This dissertation provides an end-to-end scalable equivalence checking support for behavioral synthesis. The major challenge of this research is to bridge the huge semantic gap between the ESL and RTL descriptions, which makes the direct comparison of designs in ESL and RTL difficult. Moreover, a large number and a wide variety of aggressive transformations from front-end to back-end require an end-to-end scalable checking framework. This dissertation provides an end-to-end scalable equivalence checking support for behavioral synthesis. The major challenge of this research is to bridge the huge semantic gap between the ESL and RTL descriptions, which makes the direct comparison of designs in ESL and RTL difficult. Moreover, a large number and a wide variety of aggressive transformations from front-end to back-end require an end-to-end scalable checking framework. A behavioral synthesis flow can be divided into three major phases, including 1) front-end : compiler transformations, 2) scheduling: assigning each operation a clock cycle and satisfying the user-specified constraints, and 3) back-end : local optimizations and RTL generation. In our end-to-end and incremental equivalence checking framework, we check each of the three phases one by one. Firstly, we check the front-end that consists of a sequence of compiler transformations by decomposing it into a series of checks, one for each transformation applied. We symbolically explore paths in the input and output programs of each transformation, and check whether the input and output programs have the same observable behavior under the same path condition. Secondly, we validate the scheduling transformation by checking the preservation of control and data dependencies, and the preservation of I/O timing in the user-specified scheduling mode. Thirdly, we symbolically simulate the scheduled design and the generated RTL cycle by cycle, and check the equivalence of each mapped variables. We also develop several key optimizations to make our back-end checker scale to real industrial-strength designs. In addition to the equivalence checking framework, we also present an approach to detecting deadlocks introduced by parallelization of RTL blocks that are connected by synthesized interfaces with handshaking protocols. To demonstrate the efficiency and scalability of our framework, we evaluated it on transformations applied by a behavioral synthesis tool to designs from the C-based CHStone and SystemC-based S2CBench benchmarks. Based on the evaluation results, our front-end checker can efficiently validate more than 75 percent of the total of 1008 compiler transformations applied to designs from the CHStone benchmark, taking an average time of 1.5 seconds per transformation. Our scheduling checker can validate control-data dependencies and I/O timing of all designs from S2CBench benchmark. Our back-end checker can handle designs with more than 32K lines of synthesized RTL from the CHStone benchmark, which demonstrates the scalability of the checker. Furthermore, our checker found several bugs in a commercial tool, underlining both the importance of formal equivalence checking and the effectiveness of our approach.

This thesis describes TeaBag, which is a debugger for functional logic computations. TeaBag is an accessory of a virtual machine currently under development. A distinctive feature of this machine is its operational completeness of computations, which places novel demands on a debugger. This thesis describes the features of TeaBag, in particular the handling of non-determinism, the ability to control nondeterministic steps, to remove context information, to toggle eager evaluation, and to set breakpoints on both functions and terms. This thesis also describes TeaBag's architecture and its interaction with the associated virtual machine. Finally, some debugging sessions of defective programs are presented to demonstrate TeaBag's ability to locate bugs. A distinctive feature of TeaBag is how it presents non-deterministic trace steps of an expression evaluation trace to the user. In the past expression evaluation traces were linearized via backtracking. However, the presence of backtracking makes linear traces difficult to follow. TeaBag does not present backtracking to the user. Rather TeaBag presents the trace in two parts. One part is the search space which has a tree structure and the other part is a linear sequence of steps for one path through the search space.

Abstract not available

In this thesis we propose the use of Dijkstra's concept of a predicate transformer [Dij75] for the determination of database transaction safety [SS89] and the generation of simple conditions to check that a transaction will not violate the integrity constraints in the case that it is not safe. The generation of this simple condition is something that can be done statically, thus providing a mechanism for generating safe transactions. Our approach treats a database as state, a database transaction as a program, and the database's integrity constraints as a postcondition in order to use a predicate transformer [Dij75] to generate a weakest precondition. We begin by introducing a set-oriented update language for relational databases for which a predicate transformer is then defined. Subsequently, we introduce a more powerful update language for deductive databases and define a new predicate transformer to deal with this language and the more powerful integrity constraints that can be expressed using recursive rules. Next we introduce a data model with object-oriented features including methods, inheritance and dynamic overriding. We then extend the predicate transformer to handle these new features. For each of the predicate transformers, we prove that they do indeed generate a weakest precondition for a transaction and the database integrity constraints. However, the weakest precondition generated by a predicate transformer still involves much redundant checking. For several general classes of integrity constraint, including referential integrity and functional dependencies, we prove that the weakest precondition can be substantially further simplified to avoid checking things we already know to be true under the assumption that the database currently satisfies its integrity con-straints. In addition, we propose the use of the predicate transformer in combination with meta-rules that capture the exact incremental change to the database of a particular transaction. This provides a more general approach to generating simple checks for enforcing transaction safety. We show that this approach is superior to known existing previous approaches to the problem of efficient integrity constraint checking and transaction safety for relational, deductive, and deductive object-oriented databases. Finally we demonstrate several further applications of the predicate transformer to the problems of schema constraints, dynamic integrity constraints, and determining the correctness of methods for view updates. We also show how to support transactions embedded in procedural languages such as C.

Thesis (Ph.D.)--University of Delaware, 2007. / Principal faculty advisors: Lori L. Pollock and Vijay K. Shanker, Dept. of Computer & Information Sciences. Includes bibliographical references.

Bibliography: leaves [238]-244.

Mes travaux s'articulent principalement autour de trois axes concernant la programmation sécurisée, plus particulièrement dans le cadre d'applications distribuées. Ainsi, nous considérons plusieurs participants ne se faisant pas mutuellement confiance et ayant des niveaux de sécurité différents. On s'intéresse alors au garanties restantes lorsque certains de ces participants sont compromis. Par exemple, lors d'une opération de commerce électronique, le client, le serveur, et la banque ne se font pas mutuellement confiance et font encore moins confiance aux machines intermédiaires du réseau; on veut pourtant qu'une transaction sécurisée puisse avoir lieu.

Ce manuscrit de thèse présente les travaux menés sur le système de modules de l'assistant de Preuve Coq.

Le but de cet thèse est de contribuer à rendre la programmation Web plus flexible et plus sûre qu'elle ne l'est avec les solutions répandues actuellement. Pour ceci, nous proposons une solution dans la lignée de la famille de langages ML, qui laisse un maximum de liberté au programmeur de part son côté multi-paradigmes, tout en offrant un degré de sûreté important grâce au typage statique. Dans une première partie, nous montrons qu'il est possible de programmer le navigateur sans se plier au style de JavaScript. Notre solution est OBrowser, une implantation en JavaScript de la machine virtuelle OCaml. L'implantation prend en charge l'ensemble du langage OCaml et de sa bibliothèque, y compris le modèle de concurrence préemptif. Nous présentons de plus un mécanisme d'inter-opérabilité entre les couches objet de JavaScript et d'OCaml, permettant d'utiliser de façon bien typée l'environnement du navigateur avec les objets d'OCaml. Dans une seconde partie, nous fournissons une API de manipulation du document plus sûre et de plus haut niveau que le DOM des navigateurs. En particulier, nous cherchons à éliminer les déplacements implicites effectués par le DOM pour maintenir la forme d'arbre, qui limitent les possibilités de typage statique. Nous donnons d'abord fDOM, un modèle formel minimal similaire au DOM. Puis nous proposons cDOM, un modèle alternatif ou les déplacements sont remplacés par des copies. Nous décrivons ensuite FidoML, un langage basé sur ML, permettant les manipulations bien typées du document grâce à l'utilisation de cDOM. Dans toute cette partie, nous faisons attention à ce que les solutions données soient aussi adaptables que possible. Dans une troisième partie, nous montrons comment les travaux, jusqu'ici principalement pré- sentés dans le cadre du navigateur, s'appliquent à un contexte multi-tiers. Nous donnons d'abord un tour d'horizon des plates-formes multi-tiers proches issues de la recherche. Nous décrivons en particulier les solutions qu'elles apportent à un ensemble de problématiques spécifiques à la pro- grammation Web. Puis nous concluons en présentant les grandes lignes d'un langage multi-tiers mettant à profit les travaux des deux premières parties dans les solutions à ces différentes problé- matiques.

Les systèmes basés sur la Théorie des Types prennent une importance considérable tant pour la vérification de programmes qu'en tant qu'outils permettant la preuve formelle de théorèmes mettant en jeu des calculs complexes. Ces systèmes nécessitent aujourd'hui une grande expertise pour être utilisés efficacement. Nous développons des constructions de haut niveau permettant d'utiliser les langages basés sur les théories des types dépendants aussi simplement que les langages de programmation fonctionnels usuels, sans sacrifier pour autant la richesse des constructions disponibles dans les premiers. Nous étudions un nouveau langage permettant l'écriture de programmes certifiés en ne donnant que leur squelette algorithmique et leur spécification. Le typage dans ce système donne lieu à la génération automatique d'obligations de preuve pouvant être résolues a posteriori. Nous démontrons les propriétés métathéoriques essentielles du système, dont les preuves sont partiellement mécanisées, et détaillons son implémentation dans l'assistant de preuve Coq. D'autre part, nous décrivons l'intégration et l'extension d'un système de "Type Classes" venu d'Haskell à Coq via une simple interprétation des constructions liées aux classes dans la théorie des types sous-jacente. Nous démontrons l'utilité des classes de types dépendantes pour la spécification et la preuve et présentons une implémentation économique et puissante d'une tactique de réécriture généralisée basée sur les classes. Nous concluons par la mise en œuvre de l'ensemble de ces contributions lors du développement d'une bibliothèque certifiée de manipulation d'une structure de données complexe, les "Finger Trees".