Putting Real Tools in the Hands of Students


April 14, 2011


Tom Ball, Nikolai Tilmann, and Nigel Horspool


MSR, University of Victoria


This session will look at some of the tools new coming out of Microsoft Research which can be of great interest to professors and students.

PexForFun (http://www.pex4fun.com/) can be used to learn software programming at many levels, from high school all the way through graduate courses. With PexForFun, the student edits the code in any browser – with Intellisense – and we execute it and analyze it for you in the cloud. PexForFun supports C#, VisualBasic and F#. PexForFun finds interesting and unexpected input values that help students understand what their code is actually doing. Under the hood, PexForFun uses dynamic symbolic execution to thoroughly explore feasible execution paths. The real fun starts with Coding Duels where the student has to write code that implements a specification. PexForFun finds any discrepancies between the student’s code and the specification. PexForFun connects teachers, curriculum authors and students in a unique social experience, tracking and streaming progress updates in real time.

F# is a powerful new programming language, largely based on the functional programming paradigm, which runs on .NET or Mono across the Windows, Mac and Linux platforms. It also has a very successful professional implementation in Visual Studio 2010. To provide a gentle introduction to F# and show off its capabilities, Microsoft Research is developing a number of helpful resources. The easiest one to use will not require the user to download any software to their computer, it will just require a browser. This talk will demonstrate the TryF# website, showing and solving sample programming problems which are posed on the website. Finall,y we consider how can we execute tasks in parallel if they read and write the same data? The concurrent revisions programming model allows parallel programs to remain simple, race-free and deterministic, by versioning shared state so that each task can work with an independent snapshot.


Tom Ball, Nikolai Tilmann, and Nigel Horspool

Thomas Ball is a Principal Researcher at Microsoft Research and manages the Software Reliability Research group (http://research.microsoft.com/srr/), which investigates a variety of techniques for improving software quality, including formal methods, program analysis and automated testing. He completed my Ph.D. in Computer Science from the University of Wisconsin-Madison in 1993, was a researcher at Bell Labs from 1993 to 1999 and has been at Microsoft Research since 1999.

Nikolai Tillmann. Principal Research Software Design Engineer, Microsoft Research. Nikolai Tillmann works at Microsoft Research on combining dynamic and static program analysis techniques. He currently leads the Pex project, a framework for runtime verification and automatic test-case generation for .NET applications based on parameterized unit testing and dynamic symbolic execution. He also works on the Spur project, a tracing Just-In-Time compiler for .NET and JavaScript code. Previously he worked on AsmL, an executable modeling language, and the Spec Explorer 2004 model-based testing tool. He co-developed XRT, a concrete/symbolic state exploration engine and software model-checker for .NET.

Nigel Horspool is a professor of computer science at the University of Victoria. His main focus for research and teaching has been programming languages and compilers. He is the author or co-author of three books, which cover the C language, Unix and the C# language. He is currently the co-editor of the journal ‘Software: Practice and Experience’.


  • Portrait of Tom Ball

    Tom Ball

    Research Manager/ Principal Researcher