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 |