POPL-Related Microsoft Research Technologies

Principles of Programming Languages 2012
January 25–27, 2012 | Philadelphia, PA, United States

Programming Languages, Development, and Education

Code ContractsCode Contracts provide a language-agnostic way to express coding assumptions in Microsoft .NET programs. Code Contracts tools include a runtime checker, a static checker based on abstract interpretation, and a documentation generator. See tutorial at VSTTE.

Visual F#F# 3.0 extends the succinct and expressive F# language so you can program directly against rich spaces of data and services, such as databases, web services, web data feeds, and data brokers. F# is open source under the Apache 2.0 license and is developed as a partnership between Microsoft Research and the Microsoft Visual F# team.

TouchDevelopTouchDevelop is a radically new software development environment on the Windows Phone, bringing the excitement of the first programmable personal computers to the phone. Program with TouchDevelop on Windows Phones at the Microsoft table in the foyer! 


Pex for funPex for fun brings programming in C#, Microsoft Visual Basic, and F# to your web browser. Click the Ask Pex! button to compile, run, and analyze your code by using the automatic test generation capabilities of Pex. Interactive code duels challenge you to write code that matches a secret implementation. Many teachers are using Pex for fun in their courses today.  

Verification Tools

BEK is a domain-specific language for writing common string manipulating functions and is combined with state-of-the-art analysis based on symbolic transducers (see POPL paper by Veanes et al.) With BEK, you can answer questions like: “Are these two programs equivalent?” or “Does the order matter?”

Chalice is a programming language for investigating the correctness of concurrent programs. Its specifications are based on Implicit Dynamic Frames and fractional permissions. It can be used to reason about fine-grain locks and sharing, threads, and channels. Hear more about Chalice at the POPL TutorialFest.

Dafny is an imperative, object-oriented programming language with classes and inductive datatypes, and specification constructs for describing intended behavior. The Dafny static verifier, built on Boogie, checks the consistency of the program and these specifications. Look for the Dafny Tutorial at VSTTE.

F*F* is a new verification-oriented language based on F#. Specifications in F* are stated using dependent types and its certified typechecker (see POPL paper) makes use of an SMT solver to provide a powerful, semi-automated way to certify the correctness of higher-order programs. F* compiles to .NET bytecode in a type-preserving style.

PoirotPoirot is a static analysis tool for helping programmers detect and debug errors in concurrent and asynchronous systems. Poirot can detect application-specific errors, including data races, deadlocks, assertion failures, and protocol violations. POPL paper by Joshi, Lahiri, Lal uses Poirot.

SLAyer is a program analysis tool designed to prove the absence of memory safety errors using Separation Logic. SLAyer is aimed at moderately sized (10–30K) systems-level code bases written in C; it is fully automatic and does not require annotations or hints from the programmer.

The TLA Toolbox is an IDE for writing and running debugging tools on specifications written in the TLA+ language, a very expressive high level specification language. Writing and checking TLA+ specs allow software designers to catch errors before any code is written, complementing the many tools for finding coding errors. Hear Leslie Lamport talk at LADA.

VCCVCC is an industrial-strength verification environment (deductive verifier, verification debugger, proof progress monitor, IDE integration) for low-level concurrent systems code written in C. VCC has been used to verify the functional correctness of tens of thousands of lines of commercial operating system code. Hear more about VCC at LADA and VSTTE.

Verification Infrastructure

Boogie is a first-order intermediate verification language, used by program verifiers, program checkers, and other program analyzers to formulate verification conditions (VCs). More than a dozen verification tools are built on Boogie, including VCC, HAVOC, Dafny, and Chalice. Boogie uses Z3 to discharge VCs.

Symbolic Automata is a toolkit that lifts classical automata analysis to work modulo rich alphabet theories. The toolkit supports analysis of finite symbolic automata and symbolic transducers (see POPL paper by Veanes et al.), internalizing automata as Z3 theories.

Z3Z3 is a high-performance theorem prover that supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification tools from Microsoft Research. Z3 is now available for commercial use.

Event Website
Related Microsoft Groups and Labs