Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Research in Software Engineering (RiSE)

coordinates Microsoft's Research in Software Engineering in Redmond, USA. Our mission is to advance the state of the art in Software Engineering and to bring those advances to Microsoft’s businesses.

Foundations of Correctness     

Formal Methods

Ivy, Lean, Z3Symbolic Automata, FORMULA

 Programming Languages for Verification

  Dafny, F*, Koka, P
Software Productivity    

Program Synthesis 

  BlinkFill, FlashFill

Debugging and Testing 

  Time travel debugging, automated test generation

Program Analysis 

  Corral, Duality, Angelic Verification, SymDiff 

Empirical Software Engineering

  Software Reliability, Software Process, Empirical Studies
Systems at Scale    

Cloud Correctness 

  Network Verification

Cloud Efficiency 


Retro, Processing in Memory 

 Safe Cyberphysical Systems


Working with Big Data

  Parasail, Tempe, Trill, Uncertainty

CS Education 

  BBC micro:bit, Touch Develop, Code Hunt  

Scholarly publications 




The RiSE team consists of 30+ passionate researchers and developers.


In the News


Source Code

Code Contracts for .NET
Touch Develop
Automate graph layout
Lean interactive theorem prover
Z3 automated theorem prover
Symbolic automata
Boogie intermediate verification language
P asynchronous event-driven programming
VCC Concurrent C Verifier
F* language and verifier
Dafny verification language
Zing model checker
CHESS concurrency tool


For a complete list of open source projects, see

Try RiSE tools at