Peli at RiSE

In this video, David Molnar and Margus Veanes, both Researchers at Microsoft Research, give a demo of BEK (you can try it too at http://rise4fun.com/bek). BEK is a domain specific language for writing common string functions, combined with state of the art analysis. With BEK, you can…

Интервью с Андреем Бреславым, русским аспирантом, проходившим стажеровку в MSR У MSR есть специальная программа стажировки созданная специально дла России. Здесь вы можете посмотреть интервью с Андреем Бреславым, русским…

In this episode of The Verification Corner, Kuat Yessenov and Rustan Leino, Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research,  show how a program can be constructed by stepwise refinement.  First, a high-level description of the program…

Mike Barnett and Daryl Zuniga showcase the Code Contracts Editor Extensions. The extensions integrate Code Contracts into the C# intellisense, the Code Definition View and even the editor text itself. Download the Code Contracts Editor Extensions Try Code Contracts in your browser at…

In this video, Nikolai Tillmann walks us through pexforfun.com, a website where you can write small C#, VB, or F# programs and explore them directly from your browser by using Pex. Additionally, Pex also makes it possible to play coding duels, in which users compete to discover a…

Madan Musuvathi and Sebastian Burckhardt, two Researchers at the Research in Software Engineering team (RiSE), explain and demo a new testing tool called Cuzz. As you will see in this video, Cuzz stands for "Concurrency fuzzing." Cuzz is a very effective tool for…

In this video, Mark Marron, who is visiting the Research in Software Engineering group (RiSE) for the summer, describes some work and gives a short demo on a technique for visualizing and understanding a program’s runtime memory structure (which data structures are built, how big they are, how…

Margus Veanes, a Researcher from the RiSE group at Microsoft Research, gives an overview of Rex, a tool that generates matching string from .NET regular expressions. Rex turns regular expressions into symbolic automatons, then gives them to a constraint solver to find matching strings.…

In this episode of The Verification Corner, Rustan Leino, Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, shows how to prove loop termination. During his demonstration, Rustan presents the theoretical background information necessary to build the…

In this episode of The Verification Corner, Rustan Leino gives a demonstration of specifications in action. He builds a program that chunks strings into pieces, i.e. a chunker, in Spec#. During the demo, he shows the verifier, the developer, and the specifications fit together in the development…