| Accuracy-Aware Computing |
Rinard |
Program analysis and transformation for approximate computations |
| Alloy |
Jackson |
A declarative language for modelling software systems that manipulate complex structures |
| Bedrock |
Chlipala |
An extensible low-level programming language designed to enable formal verification |
| BCL: Bluespec Codesign Language |
Arvind |
Automatic generation of HW/SW interfaces |
| Bolt |
Rinard |
Eliminating infinite loops in stripped x86 and x64 binaries |
| Cloud Intrusion Detection and Repair |
Rinard |
Security and resilience for cloud computing systems |
| Collabode |
Miller |
A web-based Java software development environment designed to support close, synchronous collaboration between two or more programmers |
| DynamoRIO |
Amarasinghe |
An efficient runtime code manipulation system |
| Input Rectification |
Rinard |
Eliminating vulnerabilities and preserving content by modifying inputs |
| Kendo |
Amarasinghe |
A deterministic multithreading library for commodity hardware |
| Micado |
Amarasinghe |
An AutoCAD plug-in for programmable microfluidic chips |
| Multi-FPGA Compiler |
Arvind |
Compiling LI-BDNs for multiple FPGA executions |
| PetaBricks |
Amarasinghe |
A language that exposes algorithmic choices to the compiler |
| Programming with Delegation |
Solar-Lezama |
Using constraints in implementations to produce robust and efficient programs |
| Program Verification for Secure Mobile Apps |
Rinard |
Static analysis for secure Android applications |
| Relaxed Programming |
Rinard |
Analysis and verification of relaxed nondeterministic programs |
| Rule-Based Power Gating |
Arvind |
Language semantics driven power gating of Bluespec programs |
| Sketch |
Solar-Lezama |
Induction-based program synthesis from implementation specifications |
| SPICE |
Rinard |
Eliminating vulnerabilities in stripped x86 and x64 binaries |
| Storyboard Programming |
Solar-Lezama |
Using abstraction and a graphical interface for usable and verifiable program synthesis |
| StreamIt |
Amarasinghe |
A high-performance language and compiler for streaming applications |
| Structural Bluespec |
Arvind |
Automatic transformation of synchronous FSM specifications into LI-BDNs |
| Synthesis from Program Traces |
Solar-Lezama |
Using a database of program behaviors to aid synthesis for complex object-oriented library code |
| Umbra |
Amarasinghe |
An efficient and scalable memory shadowing framework |
| Ur/Web |
Chlipala |
A statically typed functional programming language for Web applications, with security-by-construction and support for statically typed metaprogramming |
| Verification of Rule-Splitting Transformations in Bluespec |
Arvind |
|
| VIBRANCE |
Rinard |
Dynamic techniques for secure Java programs |
