Seminars

First order logic with transitive closure, and separation logic enable elegant interactive verification of heap-manipulating programs. However, undecidabilty results and high asymptotic complexity of checking validity preclude complete automatic verification of such programs, even when loop invariants and procedure contracts are specified as formulas in these logics. This work tackles the problem of procedure-modular verification of reachability properties of heap-manipulating programs using efficient decision procedures that are complete: that is, a SAT solver must generate a…

It is well-known that hardware implementation can outperform the software implementation of the same application, including security primitives such as encryption, by up to several magnitudes. However, hardware implementation may also make security primitives vulnerable despite their mathematical soundness. In this talk, we will discuss the role of hardware in cybersecurity.

First, we will use the finite state machine (FSM) model to demonstrate that the systems built with today's design flow and tools are vulnerable against a simple random walk attack. We further show that a…

This talk takes a retrospective look at the course of Cyber-Physical Systems, and then looks forward to challenges ahead.  There have been changes, and more are coming – some seen, some doubtless not anticipated.  But the need for, and interest in, the CPS area is only growing.  As researchers gravitate to this field, they will find opportunities to tackle new and interesting problems, both in the application domains and in the science and technology.

Synthesis is the automated construction of a system from its specification.  The system has to satisfy its specification in all possible environments. Modern systems often interact with other systems, or agents. Many times these agents have objectives of their own, other than to fail the system.  Thus, it makes sense to model system environments not as hostile, but as composed of rational agents; i.e., agents that act to achieve their own objectives.  We introduce the problem of synthesis in the context of rational agents (rational synthesis, for short).  The input consists of a temporal-…

The recent focus upon compositional design in real-time systems research has yielded a number of promising frameworks for the integration of multiple safety- and time-critical components upon a shared computational platform.  Integration of components has a profound impact upon the size and cost of the system by potentially reducing the hardware resources that must be dedicated to ensure the safe functioning of the system.  These frameworks have also introduced many interesting open research challenges such as: 1) Allocation: how do we determine the optimal interface which accurately…