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|
|Ivy, Lean, Z3, Symbolic Automata, FORMULA|
Programming Languages for Verification
|Dafny, F*, Koka, P|
Debugging and Testing
|Time travel debugging, automated test generation|
|Corral, Duality, Angelic Verification, SymDiff|
|Software Reliability, Software Process, Empirical Studies|
|Systems at Scale|
Retro, Processing in Memory
Safe Cyberphysical Systems
Working with Big Data
|Parasail, Tempe, Trill, Uncertainty|
|BBC micro:bit, Touch Develop, Code Hunt|
The RiSE team consists of 30+ passionate researchers and developers.
In the News
- Microsoft Research has been awarded the 2016 IEEE Technical Council on Software Engineering (TCSE) Distinguished Synergy Award “presented annually to a team for outstanding and/or sustained contributions that stand as a model in the software engineering community of effective partnership between industry and universities.”
- CRA Women Celebrates Women’s History Month features interview with Kathryn McKinley
- Project Premonition aims to use mosquitoes, drones, cloud computing to prevent disease outbreaks:
- ICSE 2016 Distinguished Paper Award for Guiding Dynamic Symbolic Execution Toward Unverified Program Executions by Maria Christakis and co-authors
- Maria Christakis's Ph.D. thesis was nominated by ETH for the Gesellschaft für Informatik prize for best dissertation
- SIGPLAN Research Highlight (May 2015), Parallelizing dynamic programming through rank convergence, Saeed Maleki, Madanlal Musuvathi, Todd Mytkowicz
- Nachi Nagappan named a 2015 ACM Distinguished Scientist
- The 2015 ACM Programming Languages Software Award goes to Christoph Wintersteiger, Leonardo de Moura, and Nikolaj Bjorner of MSR for their foundational work on the Z3 automated theorem prover, which powers several generations of testing, analysis and verification tools.
Guiness Book of World Records: The most people trained in computer programming in 8 hours was achieved at the 2015 Microsoft Imagine Coding Camp, an event organized by Microsoft Corporation in Redmond, WA, USA on 30 July 2015 (using www.touchdevelop.com)
SIGPLAN PLDI 2015 Distinguished Artifact Award, FlashRelate: extracting relational data from semi-structured spreadsheets using examples, Daniel W. Barowy, Sumit Gulwani, Ted Hart, and Benjamin Zorn
2014 CAV Award "For the development of partial-order reduction algorithms for efficient state-space exploration of concurrent systems", Patrice Godefroid, Doron Peled, Antti Valmari, Pierre Wolper
"Uncertain<T>: A First-Order Type for Uncertain Data," J. Bornholt, T. Mytkowicz, and K.S. McKinley, ASPLOS 2014, selected for ACM SIGPLAN Research Highlights, November 2014.
- FMCAD Best Paper Award. Akash Lal and Shaz Qadeer, A Program Transformation for Faster Goal-Directed Search, in Formal Methods in Computer-Aided Design (FMCAD), FMCAD, October 2014.
- 2014 ACM SIGMETRICS Test of Time Award, for Kathryn McKinley's paper “Myths and Realities: The Performance Impact of Garbage Collection” co-authored with Steve Blackburn and Perry Cheng which appeared originally in SIGMETRICS June 2004.
- FSE 2014 Distinguished Paper: Miltiadis Allamanis, Earl T. Barr, Christian Bird, and Charles Sutton, Learning Natural Coding Conventions
- FSE 2014 Distinguished Paper: Akask Lal, Shaz Qadeer, Powering the Static Driver Verifier using Corral
Code Contracts for .NET
|Automate graph layout||https://github.com/microsoft/automatic-graph-layout|
|Lean interactive theorem prover||https://github.com/leanprover/lean|
|Z3 automated theorem prover||https://github.com/z3prover/z3|
|Boogie intermediate verification language||https://github.com/boogie-org/boogie|
|P asynchronous event-driven programming||https://github.com/p-org/P|
|VCC Concurrent C Verifier||https://github.com/microsoft/vcc|
|F* language and verifier||https://github.com/FStarLang/FStar/|
|Dafny verification language||http://dafny.codeplex.com/|
|Zing model checker||http://zing.codeplex.com/|
|CHESS concurrency tool||http://chesstool.codeplex.com/|
For a complete list of open source projects, see http://research.microsoft.com/en-us/projects/opensource/
Try RiSE tools at www.rise4fun.com
- Rishabh Singh, BlinkFill: Semi-supervised Programming By Example for Syntactic String Transformations, in 42nd International Conference on Very Large Data Bases (VLDB 2016), VLDB – Very Large Data Bases, September 2016.
- Loris D'Antoni and Margus Veanes, Minimization of Symbolic Tree Automata, in LICS, IEEE – Institute of Electrical and Electronics Engineers, July 2016.
- Loris D'Antoni, Roopsha Samanta, and Rishabh Singh, Qlose: Program Repair with Quantiative Objectives, in 27th International Conference on Computer Aided Verification (CAV 2016), July 2016.
- Parmit K. Chilana, Rishabh Singh, and Philip J. Guo, Understanding Conversational Programmers: A Perspective from the Software Industry, in Proceedings of the 34th Conference on Human-Computer Interaction (CHI 2016), ACM – Association for Computing Machinery, May 2016.
- Thomas Ball, Jonathan Protzenko, Judith Bishop, Michał Moskal, Jonathan de Halleux, Michael Braun, Steve Hodges, and Clare Riley, Microsoft Touch Develop and the BBC micro:bit, in ICSE 2016 Companion, ACM – Association for Computing Machinery, May 2016.
- Edward K. Smith, Christian Bird, and Thomas Zimmermann, Beliefs, Practices, and Personalities of Software Engineers: A Survey in a Large Software Company, in Proceedings of the 9th International Workshop on Cooperative and Human Aspects of Software Engineering (CHASE 2016), ACM – Association for Computing Machinery, May 2016.
- Prem Devanbu, Thomas Zimmermann, and Christian Bird, Belief & Evidence in Empirical Software Engineering, in Proceedings of the 38th International Conference on Software Engineering (ICSE 2016), ACM – Association for Computing Machinery, May 2016.
- Michael Washburn Jr, Pavithra Sathiyanarayanan, Meiyappan Nagappan, Thomas Zimmermann, and Christian Bird, "What Went Right and What Went Wrong": An Analysis of 155 Postmortems from Game Development, in Proceedings of the 38th International Conference on Software Engineering (ICSE 2016 SEIP Track), ACM – Association for Computing Machinery, May 2016.
- Miryung Kim, Thomas Zimmermann, Robert DeLine, and Andrew Begel, The Emerging Role of Data Scientists on Software Development Teams, in Proceedings of the 38th International Conference on Software Engineering (ICSE 2016), ACM – Association for Computing Machinery, May 2016.
- Diego Garbevetsky, Edgardo Zoppi, Thomas Ball, and Benjamin Livshits, Toward Full Elasticity in Distributed Static Analysis, no. MSR-TR-2016-13, 23 March 2016.
- Rishabh Singh and Sumit Gulwani, Transforming Spreadsheet Data Types using Examples, in 43rd Symposium on Principles of Programming Languages (POPL 2016), ACM – Association for Computing Machinery, January 2016.
- Mikael Mayer, Gustavo Soares, Maxim Grechkin, Vu Le, Mark Marron, Oleksandr Polozov, Rishabh Singh, Benjamin Zorn, and Sumit Gulwani, User Interaction Models for Disambiguation in Programming by Example, in 28th ACM User Interface Software and Technology Symposium (UIST 2015), ACM – Association for Computing Machinery, November 2015.
- Loris D'Antoni, Margus Veanes, Benjamin Livshits, and David Molnar, Fast: A Transducer-Based Language for Tree Manipulation, in ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 38, no. 1, ACM – Association for Computing Machinery, October 2015.
- Brittany Johnson, Thomas Zimmermann, and Christian Bird, Appendix to The Effect of Work Environments on Productivity, no. MSR-TR-2015-66, 28 August 2015.
- Ankush Das, Shuvendu K. Lahiri, Akash Lal, and Yi Li, Angelic Verification: Precise Verification Modulo Unknowns, in Computer Aided Verification (CAV), Springer, July 2015.
- Loris D’Antoni and Margus Veanes, Extended symbolic finite automata and transducers, in Formal Methods in System Design , Springer, July 2015.
- Rishabh Singh and Sumit Gulwani, Predicting a Correct Program in Programming by Example, in 27th International Conference on Computer Aided Verification (CAV 2015), July 2015.
- Chris Hawblitzel, Erez Petrank, Shaz Qadeer, and Serdar Tasiran, Automated and modular refinement reasoning for concurrent programs, July 2015.
- Rajeev Alur, Dana Fisman, Rishabh Singh, and Armando Solar-Lezama, Results and Analysis of SyGuS-Comp'15, in Proceedings Fourth Workshop on Synthesis (SYNT 2015), July 2015.
- Daniel Perelman, Judith Bishop, Sumit Gulwani, and Dan Grossman, Automated Feedback and Recognition through Data Mining in Code Hunt, no. MSR-TR-2015-57, July 2015.
- Xi Yang, Stephen M. Blackburn, and Kathryn S. McKinley, Computer Performance Microscopy with SHIM, ACM/IEEE International Symposium on Computer Architecture (ISCA), June 2015.
- Tao Xie, Nikolai Tillmann, Jonathan de Halleux, and Judith Bishop, Educational Software Engineering: Where Software Engineering, Education, and Gaming Meet, pp. 115-132, CRC Press, June 2015.
- Akash Lal and Shaz Qadeer, DAG Inlining: A Decision Procedure for Reachability-Modulo-Theories in Hierarchical Programs, in Programming Language Design and Implementation (PLDI), ACM, June 2015.
- Vasileios Karakostas, Jayneel Gandhi, Furkan Ayar, Adrián Cristal, Mark D. Hill, Kathryn S. McKinley, Mario Nemirovsky, Michael M. Swift, and Osman Ünsal, Redundant Memory Mappings for Fast Access to Large Memories, ACM/IEEE International Symposium on Computer Architecture (ISCA), June 2015.
- Na Meng, Lisa Hua, Miryung Kim, and Kathryn S. McKinley, Does Automated Refactoring Obviate Systematic Editing?, ACM – Association for Computing Machinery, May 2015.
Try a Coding Duel at http://www.codehunt.com/