Profile photo of G. Edward Suh
G. Edward Suh, Ph.D.
PRECISE Seminar: High-Assurance Multi-Core Processors with Verifiable and Comprehensive Information Flow Control
February 16, 2015

As computing devices are increasingly consolidated and shared by multiple, potentially distrusting, applications, hardware must be able to provide strong isolation among software entities. For example, automative systems must be able to ensure that safety-critical control modules cannot be affected by passenger entertainment systems. In order to provide high assurance, hardware-level protection mechanisms must be verified to be implemented securely without any unintended bugs or backdoors, and be able to prevent all forms of software-visible information flows including timing channels.…

Profile photo of Sarah Loos
Sarah Loos, Ph.D.c.
PRECISE Seminar: Formal Verification of Distributed Aircraft Controllers
January 22, 2015

Formal verification and theorem proving have been used successfully in many discrete applications, such as chip design and verification.  However, computation is not confined to the discrete world of desktop computing.  Increasingly, we depend on discrete software to control safety-critical components of continuous physical systems (for example, adaptive cruise control in cars and collision avoidance in aircraft).  It is vital that these hybrid (discrete and continuous) systems behave as designed, or they will cause more damage than they intend to fix.  In this talk, I will present several…

Profile photo of Nuno Martins
Nuno Martins, Ph.D.
Joint PRECISE-GRASP Seminar: Remote and Distributed Estimation over Shared Networks - New Results and Open Problems
December 10, 2014

This talk will focus on the design of distributed estimation systems that are formed by multiple non-collocated components. A shared network is used to disseminate information among the components.

I will discuss two recent results: Assuming that the network is characterized by an incomplete directed communication graph, the first result characterizes the existence of omniscience-achieving schemes for which all components that observe only a portion of the output of an underlying plant can estimate the entire state with error that vanishes asymptotically. Our approach hinges on key…

Profile photo of Sebastian Burckhardt
Sebastian Burckhardt, Ph.D.
PRECISE Seminar: Robust Abstractions for Replicated Shared State
November 25, 2014

In the age of cloud-connected mobile devices, users want responsive apps that read and write shared data everywhere, at all times, even if network connections are slow or unavailable. Replication and eventual consistency, while able to deliver this experience, require us to face the complexity of asynchronous update propagation and conflict resolution. Our research goal is to find abstractions that encapsulate this complexity, in order to simplify the programming of distributed applications that are responsive, reactive, and collaborative.

In this talk, we first discuss the general…

Profile photo of Hamsa Balakrishnan
Hamsa Balakrishnan, Ph.D.
Joint PRECISE-GRASP Seminar: Pushback Rate Control - The Design and Field Testing of an Airport Congestion Control Algorithm
November 18, 2014

Increased congestion on the airport surface has increased taxi times, fuel consumption, and emissions. In this talk, I will describe how operational data can be used to develop and validate queuing models of airport operations. These models yield new insights on the effect of different factors such as weather, runway usage, and aircraft fleet mix on airport performance. They also help us predict the behavior of an airport under different operating conditions. 

I will then show that these queuing models can be used to design Pushback Rate Control, a new airport congestion control…