Research
Building programming languages, tools, and software engineering techniques that make software more reliable, secure, and productive.
Chalice is an experimental language that explores specification and verification of concurrency in programs. The language supports dynamic object creation, dynamic thread creation (fork and join), mutual-exclusion and readers-writers locks, monitor invariants, thread pre- and…
Boogie is an intermediate verification language, intended as a layer on which to build program verifiers for other languages. Several program verifiers have been built in this way, including the VCC and HAVOC verifiers for…
Spec Explorer is a software development tool for advanced model-based specification and conformance testing. New Version of Spec Explorer as an extension to Visual Studio is now available: Spec Explorer 2010 What are the…
FORMULA 2.0: Formal Specifications for Verification and Synthesis Formula specifications are highly declarative logic programs that can express rich synthesis and verification problems. FORMULA 2.0 is framework for formally specifying domain-specific languages (DSLs) and model…
VCC is a tool that proves correctness of annotated concurrent C programs or finds problems in them. VCC extends C with design by contract features, like pre- and postcondition as well as type invariants. Annotated…
Nozzle: Runtime heap spray detector Nozzle is a runtime monitoring infrastructure that detects attempts by attackers to spray the heap. Nozzle uses lightweight emulation techniques to detect the presence of objects that contain executable code. To…
SMT Solvers have traditionally been used for verifying correctness of systems that have been annotated with relevant inductive invariants. Such an annotation usually is an undesirable burden on the user. This project explores techniques for…