Programming languages & software engineering
Building programming languages, tools, and software engineering techniques that make software more reliable, secure, and productive.
Loopfrog: A Static Analyzer for ANSI-C Programs
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…