Programming languages & software engineering
Building programming languages, tools, and software engineering techniques that make software more reliable, secure, and productive.
New Area in Microsoft Research: Looking for a RiSE in Developer Productivity
By Rob Knies, Managing Editor, Microsoft Research In the summer of 2008, the leadership at Microsoft Research Redmond reorganized an existing set of research groups with a refreshed, more encompassing mandate: reinventing all aspects of…
Dafny: A Language and Program Verifier for Functional Correctness
Dafny is a programming language with built-in specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs. The Dafny programming language is designed to support the static verification…
Chalice
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: An Intermediate Verification Language
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…
Model-based Testing with SpecExplorer
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 – Modeling Foundations
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: A Verifier for Concurrent C
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…