Software Engineering Research

Josh Phillips(PM), Niklas Gustafsson(Architect), and Artur Laksberg(Developer) of the Parallel Computing Platform Team spend some time with me to discuss a managed (.NET-based) DSL (Domain Specific Language) for concurrent programming, Maestro. Maestro incorporates well-entrenched language…

Nikolai Tillmann and Peli de Halleux give a short tutorial on Pex, an automated white box testing tool for .Net. The tutorial is a pair-programming session where they show us how to get started with Pex in Visual Studio, starting from an (untested) piece of C# code: how to use…

A few years ago I got the chance to learn about Software Transactional Memory for the first time while visiting MSR Cambridge. The great Simon Peyton-Jones and Tim Harris explained to me the thinking behind STM and how it might evolve. It was a tremendously interesting…

CHESS is an automated tool from Microsoft Research for finding errors in multithreaded software by systematic exploration of thread schedules. It finds errors, such as data-races, deadlocks, hangs, and data-corruption induced access violations, that are extremely hard to find with…

Mike Barnett and Daryl Zuniga, a high school intern at RiSE, sit down to talk about Code Contracts for .NET and documentation. Daryl has been working this summer on a tool that inserts contracts elements into the Xml Documentation files generated by the C#/VB…

Mike Barnett gives a step-by-step tutorial on Code Contracts, a new way to express preconditions, postconditions and invariants in any .NET language. The contracts team have built a runtime instrumentation tool and also advanced static checkers that can understand and reason about…

Grigore Rosu is an associate professor in the Department of Computer Science at the University of Illinois at Urbana-Champaign (UIUC), where he leads the Formal Systems Laboratory (FSL). His research interests encompass both theoretical foundations and system development in the areas of formal…

Nikolaj Bjørner and Leonardo de Moura are Researchers in the Research in Software Engineering (RiSE) team at Microsoft Research. They are talking and demoing Z3, a high-performance SMT constraint solver. Solving constraint systems is the root of of many software…

Michal Moskal gives us a short introduction at the Verifying C Compiler (VCC) project. 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…

Today we talk with Ethan Jackson about Cloud applications.  Cloud applications are web-based distributed systems deployed over a fluctuating set of computing nodes and services. The design of cloud applications is particularly challenging because few assumptions can be made about the…