Programming languages and software engineering
Microsoft Research Blog
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…
Project
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…
Project
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…
Project
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…