Arccos
The goal of this project is to provide strong guarantees about the High-Level Sythesis process (HLS). As a starting point, we are exploring the idea of performing translation validation for HLS, which consists of showing, for each translation that the HLS tool performs, that the output program produced by the tool has the same behavior as the original program. [read more...]

Arcum
Arcum is an extension to the refactoring paradigm that provides for the modular maintenance of crosscutting design idioms, supporting both substitutability of design idiom implementations and the checking of essential constraints. [read more...]

Collider
The Collider project investigates techniques for automatically generating efficient, scalable, correct, and precise dataflow analyzers and optimizers from a very high-level specification. [read more...]

Quail
The goal of the Quail project is to develop techniques for deep typechecking and refactoring for systems that combine Java code with a database back-end using the Java Persistence API. [read more...]

Liquid Types
Liquid Types is a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. [read more...]

Radar
The Radar project aims to automatically generate precise and scalable concurrent analyses from their sequential counterparts, thereby making concurrent analyses much easier to write, and allowing compiler writers and analysis writers to easily adapt current analyses to account for concurrency. [read more...]

Javascript Security
The goal of this project is to use program analysis techniques to improve the reliability and security of Javascript code. [read more...]