Seminars

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 traffic participants, but understanding attention patterns can also be beneficial for entertainment services. In this talk, I will discuss our work towards mobile devices that can accurately track user attention - from devices that determine when we drive, over devices that recognize their users by touch, to devices that…

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 outcomes. In this talk, I will discuss several algorithmic approaches that have been developed to identify cooperative strategies in non-cooperative games.  I will describe an analysis of value-function-based reinforcement learning, the pivotal role of assumptions about the opponent, the computational benefits of side…

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 programmer omits synchronization constructs. The synthesizer fills in the appropriate synchronization to keep the program correct. However, a major hurdle to adoption of these techniques is the performance of the synthesized program. In this talk, I will present two different approaches we have explored for making synthesis for…

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 microsystems is to transduce a physiological parameter relevant to a disease state of interest, and wirelessly communicate this parameter external to the body to guide therapy. For chronic disease states, long-term, permanent sensors are of interest; while for acute disease states, biodegradable wireless microsystems may be of…

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…