The PLM group seeks to improve software development productivity through the design of new programming language features, in conjunction with program verification. The group was recently formed from members of the SPT and FSE groups.
 

From left to right: Rustan Leino, Manuel Fähndrich, Mike Barnett, Wolfram Schulte, Daan Leijen, Francesco Logozzo, Herman Venter, and Peter Müller.

Michał Moskal

Michael Carbin

Pietro Ferrara

• Spec# (pronounced "speck-sharp") is an experimental extension to C# that adds design-by-contract features. Contracts include method preconditions, postconditions, and object invariants. Contracts capture programmer intentions about how methods and data are to be used. The Spec# compiler emits run-time checks that enforce the contracts and the Spec# program verifier uses theorem-proving technology to statically check the consistency between a program and its contracts. Spec# helps programmers write correct software and makes explicit the correct usage of APIs for clients. It is integrated into Visual Studio .NET. For more information consult the Spec# project website.
• Sing# is the source language and compiler for the Singularity project. It is an experimental extension to Spec# that supports features required for writing operating systems code as well as application code running on Singularity. The main novel feature is support for message passing in the form of channel contracts and channel operations, such as blocking message receipt patterns. Additionally, the language supports explicit, but compile-time checked, memory management. This enables efficient transfer of data between communicating processes without copying, yet without the drawbacks or errors associated with shared memory.
• The Task Parallel Library is a concurrency library for C# (shipping soon with .NET)
   

For publications, see the websites of the projects and PLM members.

If you are interested in seeking job opportunities in the PLM research group, please contact Rustan Leino. Also, see the Recruiting Web Page for the Programming Languages and Tools area.

We are always looking for exceptional PhD candidates to join us as interns, especially during the summer months. For more information about becoming an intern, please visit our internship website.

Burkhart Wolff

Rosemary Monahan

Arnd Poetzsch-Heffter

Edsko de Vries

Ronald Middelkoop

Diego Garbervetsky

Jan Smans

Ralf Sasse