| Project | Faculty | Description |
|---|---|---|
| Principles of Parallel Computing | Umut Acar | |
| Data Centric Computation | Umut Acar | |
| Semantics of Concurrent Programs | Stephen Brookes | Denotational semantics for weak memory concurrency and logics for proving program correctness |
| Typecoin | Karl Crary | Peer-to-peer linear commitment using the Bitcoin network |
| Languages (1,2) for Computer Music | Roger Dannenberg | Programming languages to address timing, gestural control, concurrency, and signal processing for computer music applications |
| Security, Privacy, and Inference | Matt Fredrikson | Formal approaches for reasoning about security and privacy in statistical learning applications |
| Models for Privacy-Aware Programming | Matt Fredrikson | Theory, tools, and language-based techniques that simplify the task of writing correct privacy-aware code |
| Higher Type Theory | Robert Harper | Theory and application of higher type theory |
| Resource Aware ML | Jan Hoffmann | A programming language that statically infers symbolic resource-usage bounds |
| CURB | Jan Hoffmann | A DARPA STAC project that uses resource bounds to detect space/time vulnerabilities in Java bytecode |
| Session-Typed Concurrency | Frank Pfenning, Stephanie Balzer | Programming languages and logics based on session-typed message-passing concurrent computation |
| KeYmaera X | André Platzer | KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems |
| Logical Foundations of CPS | André Platzer | Develops logical foundations for cyber-physical systems, i.e., systems that combine cyber aspects such as communication and computer control with physical aspects such as movement in space |
| HA-Spiral | André Platzer | Verified synthesis of high assurance implementations of controllers for vehicular systems |
| Policy-Agnostic Programming | Jean Yang | A programming model for separating privacy and security policies from other computations |