About

Jonathan "Peli" de Halleux is actively working on TouchDevelop and Code Hunt. In the past, Peli worked on Moles (shipped as Fakes in Visual Studio 2012), rise4fun, Pex and Code Digger. Every morning, Peli teaches mobile computer science at his local high school.

Peli joined the Foundations for Software Engineering in October 2006. Peli worked in the CLR as a SDET in charge of the Just In Time compiler (2004-2006). Before joining Microsoft, Peli earned a PhD in Applied Mathematics from the Catholic University of Louvain (2000-2004).

Projects

Microsoft MakeCode

Established: September 1, 2016

Microsoft MakeCode is a joint project between Microsoft Research and Developer Division to make it simple to program microcontroller-based devices using a modern web app.  In addition to standing up programming environments for our hardware partners, we work closely with academia on a number of projects:

Code Hunt Community

Established: July 17, 2015

Code Hunt is a serious educational game. The Code Hunt community is interested in all aspects of research and development around the game, including analysis of the data and development of the platform. Join the Community Get updates. Tell us what you are doing. Sign up here. Announcing CHESE 2016 The 2nd Int’l Code Hunt Workshop on Educational Software Engineering (CHESE 2016) will be held in Seattle, WA, on November 18 in conjunction with FSE…

The BBC micro:bit and Microsoft

Established: May 28, 2015

Try our Block/JavaScript editor! The BBC and partners, including Microsoft, announce the BBC micro:bit – a pocket-sized, codeable computer that allows children to get creative with technology. Up to 1 million micro:bits will be given to every 11 or 12 year old child in Year 7 or equivalent across the UK, for free. “The simple truth is, being a maker matters. Real computing, doing not just consuming, will drive a creative revolution in this country.…

Code Hunt

Established: February 4, 2015

Code Hunt is a serious gaming platform for coding contests and practicing programming skills. It is based on the symbolic white box execution engine, Pex. Code Hunt is unique as an online coding platform in that each puzzle is presented with test cases only, no specification. Players have to first work out the pattern and then code the answer. Code Hunt has been used by over 350,000 players as of August 2016. Data from the…

Code Hunt Workshops

Established: February 1, 2015

1st Code Hunt Workshop, Redmond February, 15-16, 2015 Slides and Videos Deep Dive into Pex for Code Hunt Nikolai Tillmann [Slides] [Video] Code Hunt Contest Analytics Judith Bishop [Slides] [Video] Model Counting for Test Coverage in Code Hunt  Willem Visser [Slides] [Video] (after Bishop) Hint generation in Code Hunt  Daniel Perelman [Slides] [Video] A system for C programming  Amey Karkare [Slides] [Video] Semantic Clustering of Student Solutions at Scale Rishabh Singh [Video] (after Karkare) Automatic…

Pex4Fun

Established: June 6, 2013

Pex4Fun is a browser-based teaching and learning environment targeting teachers and students for introductory to advanced programming or software engineering courses. At the core of the platform is an automated grading engine based on symbolic execution. In Pex4Fun, teachers can create virtual classrooms, customize existing courses, and publish new learning material including learning games. Try it out on the web Go to www.pex4fun.com, and click Learn to start tutorials.

TouchDevelop

Established: July 20, 2011

Create apps everywhere on all your devices! For Windows Phone and the web. In the TouchDevelop programming environment you write scripts by tapping on the screen. You do not need a separate PC or keyboard. Scripts can perform various tasks similar to regular apps. Any TouchDevelop user can install, run, edit, publish scripts. You can share scripts with other people by publishing them to the TouchDevelop script bazaar, or by submitting them as an app…

TouchStudio

Established: March 15, 2011

This project has been renamed to TouchDevelop. Please visit the new Microsoft Research project website and see what scripts people write on touchdevelop.com.   Videos Watch the Channel 9 video to learn how to Script Your Phone ON Your Phone! Our good friends from Channel 9 helped us to re-record this movie.     What other people say Social Times: Microsoft Research TouchStudio Makes Windows Phone a Game Changing Platform: Prepare to be Amazed Geek Wire: Microsoft ‘TouchStudio’…

Rex – Regular Expression Exploration

Established: March 27, 2010

Rex is a tool that explores .NET regexes and generates members efficiently. Try out Rex in duel mode at http://rise4fun.com/rex! The duel mode is a game where you have to guess a secret (hidden) regex. On each attempt, Rex generates strings that match or don't match the same way as the secret regex. The game uses the ASCII range of characters, i.e. characters from code 0 to 127 and displays various automata associated to the regexes. How does the…

Moles – Isolation framework for .NET

Established: January 25, 2010

Moles allows to replace any .NET method with a delegate. Moles supports static or non-virtual methods. Moles works well with Pex. The Fakes Framework in Visual Studio 2012 is the next generation of Moles & Stubs. Fakes is different from Moles, however, so moving from Moles to Fakes will require some modifications to your code. The Moles framework will not be supported in Visual Studio 2012. Read the blog post from Peter Provost about Stubs. Read the blog…

The Verification Corner

Established: January 8, 2010

The Verification Corner is a video series on YouTube that explains different concepts of software verification.   Stepwise refinement - 10/8/2010: In this episode, 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. YouTube video Channel9 Movie and Podcasts Chalice Sources [zip]   Loop Termination - 3/29/2010: In this episode, Rustan Leino shows how to prove loop…

Stubs – Lightweight Test Stubs for .NET

Established: March 19, 2009

Stubs is a lightweight framework for .NET that provides test stubs. For interfaces and non-sealed classes, type-safe wrappers are generated that can be easily customized by attaching delegates. Stubs are part of Moles, and work well together with Pex. Stubs is a lightweight framework for test stubs in .NET that is entirely based on delegates. Stubs may be used on interfaces, abstract classes or non-sealed classes. Stubs was designed provide a minimal overhead to the Pex white…

Dafny: A Language and Program Verifier for Functional Correctness

Established: December 23, 2008

Dafny is a programming language with built-in specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs. The Dafny programming language is designed to support the static verification of programs. It is imperative, sequential, supports generic classes, dynamic allocation, and inductive datatypes, and builds in specification constructs. The specifications include pre- and postconditions, frame specifications (read and write sets), and termination metrics. To further support specifications, the language also offers…

CHESS: Find and Reproduce Heisenbugs in Concurrent Programs

Established: October 1, 2008

CHESS is a tool for finding and reproducing Heisenbugs in concurrent programs. CHESS repeatedly runs a concurrent test ensuring that every run takes a different interleaving. If an interleaving results in an error, CHESS can reproduce the interleaving for improved debugging. CHESS is available for both managed and native programs.

Pex and Moles – Isolation and White Box Unit Testing for .NET

Established: February 21, 2007

Pex automatically generates test suites with high code coverage using automated white box analysis. Pex is a Visual Studio add-in for testing .NET Framework applications. Moles supports unit testing by providing isolation by way of detours and stubs. The Moles framework is provided with Pex, or can be installed by itself as a Microsoft Visual Studio add-in. NEW: IntelliTest in Visual Studio 2015 is the evolution of Pex. IntelliTest is a feature integrated in Visual…

SLAM

Established: November 5, 2001

SLAM is a project for checking that software satisfies critical behavioral properties of the interfaces it uses and to aid software engineers in designing interfaces and software that ensure reliable and correct functioning. Static Driver Verifier is a tool in the Windows Driver Development Kit that uses the SLAM verification engine. "Things like even software verification, this has been the Holy Grail of computer science for many decades but now in some very key areas,…

Publications

2016

2015

2014

2013

2012

2011

2010

2009

2008

Projects

Link description

Keynote: The Future of Software Engineering

Date

April 14, 2011

Speakers

Wolfram Schulte, Peli de Halleux, and Nicholai Tilman

Affiliation

Manager, Software Engineering, Microsoft Research, Redmond, USA, Microsoft

Downloads

Microsoft uploader for BBC micro:bit

October 2015

    Click the icon to access this download

  • Website

Other

Volunteering

Peli teaches computer science at Rainier Beach High School every morning, as part of the TEALS program. Peli had the chance to be featured in an article of the New York Times about TEALS. In collaboration with Michael Braun at Rainier Beach, Peli co-organized AppDay, a high school event where 900 students enjoyed coding for a day. Read the GeekWire articles about this program from 2014 and 2013.

Geek of the Week

Twice, Peli was selected as geek of the week. You can read about it here and here.

Old Personal Projects

  • Creator of MbUnit, an extensible unit test framework for .Net that integrated features such as combinatorial testing.
  • QuickGraph, a library for graph data structures and algorithm in .NET,
  • Reflector Addin’s, a set of specialized modules for Reflector that range from type graph, code complexity, code review, treemap of types, statement graphs, an attempt at automatic test case generation from a method basic block graph, etc..
  • Stuff, ranging from Ant Colony Optimization, autonomous behaviors, a framework for performance tests or an attempt at literate documentation in C#.