No description available.

No description available.

No description available.

No description available.

No description available.

No description available.

We present a generic proof methodology to automatically prove correctness of design transformations introduced at the Register-Transfer Level (RTL) to achieve lower power dissipation in hardware systems. We also introduce a new algorithm to reduce switching activity power dissipation in microprocessors. We further apply our technique in a completely different domain of dynamic power management of Systems-on-Chip (SoCs). We demonstrate our methodology on real-life circuits. In this thesis, we address the dual problem of transforming hardware systems at higher levels of abstraction to achieve lower power dissipation, and a reliable way to verify the correctness of the afore-mentioned transformations. The thesis is in three parts. The first part introduces Instruction-driven Slicing, a new algorithm to automatically introduce RTL/System level annotations in microprocessors to achieve lower switching power dissipation. The second part introduces Dedicated Rewriting, a rewriting based generic proof methodology to automatically prove correctness of such high-level transformations for lowering power dissipation. The third part implements dedicated rewriting in the context of dynamically managing power dissipation of mobile and hand-held devices. We first present instruction-driven slicing, a new technique for annotating microprocessor descriptions at the Register Transfer Level in order to achieve lower power dissipation. Our technique automatically annotates existing RTL code to optimize the circuit for lowering power dissipated by switching activity. Our technique can be applied at the architectural level as well, achieving similar power gains. We first demonstrate our technique on architectural and RTL models of a 32-bit OpenRISC pipelined processor (OR1200), showing power gains for the SPEC2000 benchmarks. These annotations achieve reduction in power dissipation by changing the logic of the design. We further extend our technique to an out-of-order superscalar core and demonstrate power gains for the same SPEC2000 benchmarks on architectural and RTL models of PUMA, a fixed point out-of-order PowerPC microprocessor. We next present dedicated rewriting, a novel technique to automatically prove the correctness of low power transformations in hardware systems described at the Register Transfer Level. We guarantee the correctness of any low power transformation by providing a functional equivalence proof of the hardware design before and after the transformation. Dedicated rewriting is a highly automated deductive verification technique specially honed for proving correctness of low power transformations. We provide a notion of equivalence and establish the equivalence proof within our dedicated rewriting system. We demonstrate our technique on a non-trivial case study. We show equivalence of a Verilog RTL implementation of a Viterbi decoder, a component of the DRM System-On-Chip (SoC), before and after the application of multiple low power transformations. We next apply dedicated rewriting to a broader context of holistic power management of SoCs. This in turn creates a self-checking system and will automatically flag conflicting constraints or rules. Our system will manage power constraint rules using dedicated rewriting specially honed for dynamic power management of SoC designs. Together, this provides a common platform and representation to seamlessly cooperate between hardware and software constraints to achieve maximum platform power optimization dynamically during execution. We demonstrate our technique in multiple contexts on an SoC design of the state-of-the-art next generation Intel smartphone platform. Finally, we give a proof of instruction-driven slicing. We first prove that the annotations automatically introduced in the OR1200 processor preserve the original functionality of the machine using the ACL2 theorem prover. Then we establish the same proof within our dedicated rewriting system, and discuss the merits of such a technique and a framework. In the context of today's shrinking hardware and mobile internet devices, lowering power dissipation is a key problem. Verifying the correctness of transformations which achieve that is usually a time-consuming affair. Automatic and reliable methods of verification that are easy to use are extremely important. In this thesis we have presented one such transformation, and a generic framework to prove correctness of that and similar transformations. Our methodology is constructed in a manner that easily and seamlessly fits into the design cycle of creating complicated hardware systems. Our technique is also general enough to be applied in a completely different context of dynamic power management of mobile and hand-held devices. / text

Dieser Bericht präsentiert RACR-NET, eine Schnittstelle der Referenzattributgrammatik-gesteuerten Graphersetzungsbibliothek RACR für C#. RACR-NET ermöglicht die Nutzung der deklarativen, dynamischen Sprachspezifikations-, Instanziierungs- und Auswertungsmeachanismen der RACR Scheme-Bibliothek in der objektorientierten Programmierung. Dies umfasst insbesondere die automatische inkrementelle Auswertung attributbasierter semantischer Analysen und somit das automatische Cachen parametrisierter Funktionsmethoden. Graphersetzungen entsprechen hierbei Zustandsänderungen von Objektinstanzen und der Invalidierung abgeleiteter Berechnungen. Schwerpunkt dieses Berichts ist die objektorientierte Programmierschnittstelle von RACR-NET, dessen praktische Anwendung und Implementierung. Der Bericht ist ein Referenzhandbuch für RACR-NET Anwender und Entwickler.

Cette thèse traite de la conception de méthodes automatisées ou semi-automatisées pour détecter et identifier des algorithmes cryptographiques dans des programmes compilés en langage machine. La première méthode proposée a pour but l'identification de primitives symétriques. L'implémentation en langage machine d'une primitive symétrique, assimilée à une suite d'instructions, est représentée par un graphe. Sous cette forme, le code est modifié à l'aide de règles de réécriture tout en préservant une certaine notion de sémantique lors d'une phase dite de normalisation. L'objectif est de faire émerger des expressions communes à différentes implémentations d'une même primitive. Ces expressions servent alors de base à la création de signatures efficaces. La recherche de ces signatures s'effectue à l'aide d'un algorithme énumérant les isomorphismes de sous-graphe. La seconde méthode, conçue en complément de la première, produit une représentation synthétique facilitant l'identification des modes opératoires. Cette représentation se définit comme le plus petit sous-graphe préservant les distances entre des sous-ensembles de nœuds précédemment identifiés comme étant les paramètres d'entrée et de sortie des primitives impliquées. / This thesis is about the design of automatic or semi-automatic methods to detect and identify cryptographic algorithms inside programs compiled into machine code. Two methods are presented. The objective of the first method is to identify cryptographic primitives. A machine code implementation of a cryptographic primitive, regarded as a sequence of instructions, is represented by a graph structure. During a normalization phase, a set of rewrite rules is used to modify this graph representation while preserving a specific notion of semantics. The goal is to converge towards expressions which are shared across several implementations of the same primitive. We use these expressions as a basis to create efficient signatures. A subgraph isomorphism enumeration algorithm is used to search for signatures. The second method is built on top of the first one. It produces a synthetic representation designed to help in the identification of modes of operation. This synthetic representation is defined as the smallest subgraph which preserve distances between sets of vertices previously identified as the input and output parameters of the primitives involved within the mode of operation.

Tesis por compendio / [ES] Erlang es un lenguaje de programación funcional con concurrencia mediante paso de mensajes basado en el modelo de actores. Éstas y otras características lo hacen especialmente adecuado para aplicaciones distribuidas en tiempo real acrítico. En los últimos años, la popularidad de Erlang ha aumentado debido a la demanda de servicios concurrentes. No obstante, desarrollar sistemas Erlang libres de errores es un reto considerable. A pesar de que Erlang evita muchos problemas por diseño (por ejemplo, puntos muertos), algunos otros problemas pueden aparecer. En este contexto, las técnicas de testing y depuración basadas en métodos formales pueden ser útiles para detectar, localizar y arreglar errores de programación en Erlang. En esta tesis proponemos varios métodos para testing y depuración en Erlang. En particular, estos métodos están basados en modelos semánticos para concolic testing, pruebas basadas en propiedades, depuración reversible con consistencia causal y repetición reversible con consistencia causal de programas Erlang. Además, probamos formalmente las principales propiedades de nuestras propuestas y diseñamos herramientas de código abierto que implementan estos métodos. / [CA] Erlang és un llenguatge de programació funcional amb concurrència mitjançant pas de missatges basat en el model d'actors. Estes i altres característiques el fan especialment adequat per a aplicacions distribuïdes en temps real acrític. En els últims anys, la popularitat d'Erlang ha augmentat degut a la demanda de servicis concurrents. No obstant, desenvolupar sistemes Erlang lliures d'errors és un repte considerable. Encara que Erlang evita molts problemes per disseny (per exemple, punts morts), alguns altres problemes poden aparéixer. En este context, les tècniques de testing y depuració basades en mètodes formals poden ser útils per a detectar, localitzar y arreglar errors de programació en Erlang. En esta tesis proposem diversos mètodes per a testing i depuració en Erlang. En particular, estos mètodes estan basats en models semàntics per a concolic testing, testing basat en propietats, depuració reversible amb consistència causal i repetició reversible amb consistència causal de programes Erlang. A més, provem formalment les principals propietats de les nostres propostes i dissenyem ferramentes de codi obert que implementen estos mètodes. / [EN] Erlang is a message-passing concurrent, functional programming language based on the actor model. These and other features make it especially appropriate for distributed, soft real-time applications. In the recent years, Erlang's popularity has increased due to the demand for concurrent services. However, developing error-free systems in Erlang is quite a challenge. Although Erlang avoids many problems by design (e.g., deadlocks), some other problems may appear. Here, testing and debugging techniques based on formal methods may be helpful to detect, locate and fix programming errors in Erlang. In this thesis we propose several methods for testing and debugging in Erlang. In particular, these methods are based on semantics models for concolic testing, property-based testing, causal-consistent reversible debugging and causal-consistent replay debugging of Erlang programs. We formally prove the main properties of our proposals and design open-source tools that implement these methods. / Palacios Corella, A. (2020). Formal Methods for Constraint-Based Testing and Reversible Debugging in Erlang [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/139076 / Compendio