1. Scheduling Protocols

    Interactions amongst different processes in concurrent software are governed by a protocol. The blocking I/O operations involved in a protocol may temporarily suspend the execution of some processes in an application. Scheduling consists of the allocation of available processors to the appropriate non-suspended processes in an application, such that …

    read more
  2. Problem of coordination in cyber-physical system

    The design and analysis of cyber-physical systems bring many challenges, some of them resulting from the difficulty to express within the same formalism the interaction between discrete (cyber) and continuous (physical) processes. We propose in this work a component based description of cyber-physical systems. Components abstract from internal operations of …

    read more
  3. Erasable PUFs: Formal Treatment and Generic Design

    Physical Unclonable Functions (PUFs) have not only been suggested as new key storage mechanism, but in the form of so-called "Strong PUF" also as cryptographic primitives in advanced schemes, including key exchange, oblivious transfer, or secure multiparty computation. This notably extends their application spectrum, and has led to a sequence …

    read more
  4. Toward Secure Computing Environments

    I will briefly explain the development of secure processor architectures in industry and academia – in particular, the impact of the Aegis and Ascend architectures in 2003 and 2012. This teaches us that minimizing the Trusted Computing Base in any architecture or system is a HW/SW/Crypto co-design in which …

    read more
  5. History-based Specification and Verification of Java Collections in KeY

    In this feasibility study we discuss reasoning about the correctness of Java interfaces using histories, with a particular application to Java's Collection interface. We introduce a new specification method (in the KeY theorem prover) using histories, that record method invocations and their parameters on an interface. We outline the challenges …

    read more
  6. Overview of the Reowolf Project

    The Reowolf project introduces connectors as a replacement for BSD-style sockets for multi-party network programming. Connectors encourage applications to make explicit their requirements on the behavior of the session, by facilitating configuration using protocol code, expressed in a domain-specific protocol language (based on Reo). These protocols are retained, and shared …

    read more
  7. Discourje: Runtime Verification of Communication Protocols in Clojure

    This talk presents Discourje: a runtime verification framework for communication protocols in Clojure. Discourje guarantees safety of protocol implementations relative to specifications, based on an expressive new version of multiparty session types. The framework has a formal foundation and is itself implemented in Clojure to offer a seamless specification-implementation experience …

    read more
  8. Two Dimensional Turing Machines

    Turing in his immortal 1936 paper observed that “computing is normally done by writing… symbols on [two-dimensional] paper”, but that “the two-dimensional character of paper is no essential of computation.” I believe that the two-dimensional model is in fact much more intuitive than the standard one-dimensional version that we teach …

    read more

« Page 2 / 31 »

hosted by