Research

My goal is to make program development easier, and less error prone. As a result, I'm interested in programming language design, static type systems, program analysis and verification, as well as runtime techniques and optimizations.

Projects

Below are a list of projects I have been involved in.

Code Contracts for .NET

Documenting design decisions and coding assumptions is crucial to make code maintainable, testable, and interoperable. Code contracts are pre-conditions, post-conditions, and object invariants that document such decisions in a standardized, language-agnostic, persisted, and machine-readable form. Our tools use this format to perform runtime contract checking, static verification, and documentation generation.

Contracts will be available starting with version 4.0 of the CLR.

System C#

What features are needed to program system software, such as device drivers? This project explores how to provide safe yet efficient access to underlying memory buffers from safe client code.

Singularity/Sing#

Is it possible to write an operating system from scratch in a high-level, type and memory safe language with garbage collection? The Singularity project explores these issues and solutions. As part of the project, I designed language extensions into a language called Sing# for declaring message protocols and safe explicit memory management.

Spec#

Spec# is a derivative of C#, adding support for declaring pre-conditions, post-conditions, and object invariants in method signatures and types. The Spec# compiler generates runtime checking for these contracts. In addition, the Boogie program verifier uses theorem proving to statically reason whether the code corresponds to the declared contracts.

My main contribution to the project is the non-null type system and static checker. In Spec#, any use of a reference type can be annotated with a !, as in string! to make it explicit that the reference cannot be null. This way, the type checker provides early feedback on potential null errors.

Fugue

Is your software baroque? Fugue is an attribute based annotation language for .NET to express type states of objects. Object type states abstractly describe what state an object is in. These states influence what operations can be performed on an object. Declarations permit relating abstract type states with concrete object states. The Fugue checker statically verifies that code satisfies the declared type state constraints.

Vault

Low-level system code, such as device drivers are difficult to write. One reason for this is that the interaction of a driver with the operating system is goverend by complicated rules. Vault is a research language where such rules can be encoded as protocols in the type system and code can be statically checked against the protocol. Examples of interaction rules are maintaining proper interrupt levels, not calling certain functions at wrong interrupt levels, as well as properly handling Io request packets. As a proof of concept, we ported a floppy driver to Vault and verified these properties.

See all publications.

Organization

• Member of RiSE
• Manager of PLA
• Publications