Event Listing

User interface code can be complex and buggy.  Moreover, designing user-friendly interfaces can be difficult.   One way around this is is to reuse interfaces others have written and tested.  We are developing a framework whereby the user provides a sketch of the desired… Read more

(Joint work with Konstantinos Gatsis) The interaction between information technology and physical world makes Cyber-Physical Systems (CPS) vulnerable to malicious attacks beyond the standard cyber attacks. This has motivated the need for attack-resilient… Read more

(Joint work with Miroslav Pajic) We consider a wireless networked control system with multiple loops closing over a shared wireless medium. To avoid interferences a centralized scheduler decides which control task accesses the channel at each time step,… Read more

This talk covers several results focused on humans interacting with Cyber-Physical Systems: those systems whose computation, control, and communication aspects are tightly coupled. Human inputs to these systems has typically required significant training, which reduces the… Read more

Building safety-critical real-time systems out of inexpensive, non-realtime, COTS components is challenging. Although COTS components generally offer high performance, they can occasionally incur significant timing delays. To prevent this, we propose two approaches: 1) a new… Read more

It has long been recognized that ubiquitous information access brings enormous benefits but also creates a plethora of devices and services that are competing for our attention. With mobile devices this is a particular serious concern for drivers, pedestrians, and other… Read more

Compared to typical single-agent decision problems, general sum games offer a panoply of strategies for maximizing utiity. In many games, such as the well-known Prisoner's dilemma, agents must work together, bearing some individual risk, to arrive at mutually beneficial… Read more

Partial-program synthesis is a technique that allows programmer to specify only part of the program imperatively and the rest of the requirements declaratively. In the domain of concurrency, the input usually consists of a non-deterministic partial program where the… Read more

The tremendous technological convergence of microfabrication technology, wireless communication technology, and low-power circuitry has opened the possibility of widespread use of microfabricated implantable wireless microsystems. A typical operational mode for these… Read more

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… Read more