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.
We are organized in five working groups spanning Compilers and Runtimes, Empirical Software Engineering, Formal Methods, Program Analysis, and Programming Languages, working on a variety of themes/projects:
Modeling and Design
|Advanced Graph Layout, DKAL, Formula|
|Automatic test generation, Moles, Pex|
|RobustHeap, ToleRace, Yarra|
|Automata, BEK, Duality, Rex, SymDiff, Z3|
Concurrency & Parallelism
Measurement and Prediction
In the News
- NY Times's Fostering Tech Talent in Schools features the work of Peli de Halleux, teaching TouchDevelop in Seattle high schools as part of the TEALS program.
- CNN Money "Excel 2013’s coolest new feature that should have been available years ago" describes Flash Fill, the result of Sumit Gulwani's work on program synthesis for end-users.
- The Zing model checker, from Shaz Qadeer and Sriram Rajamani, used for verifying USB 3.0 protocols in Windows 8.
- Most Influential PLDI Paper Award (2012): Extended Static Checking for Java, Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata
- Most Influential OOPSLA Paper Award (2012): Reconsidering Custom Memory Allocation, Emery Berger, Benjamin G. Zorn, and Kathryn S. McKinley
- FSE Distinguished Paper Award (2012): Assessing the Value of Branches with What-if Analysis, Christian Bird and Thomas Zimmermann
- ICSE Software Engineering in Practice Best Paper Award (2012): Characterizing and Predicting Which Bugs Get Reopened, Thomas Zimmermann, Nachiappan Nagappan, Philip J. Guo, Brendan Murphy
- Synthesis from Examples: Interaction Models and Algorithms, SYNASC 2012, Sumit Gulwani
- Spreadsheet Data Manipulation using Examples, CACM 2012, Sumit Gulwani, William Harris, Rishabh Singh
- TouchDevelop - Programming Cloud-Connected Mobile Devices via Touchscreen, Nikolai Tillmann, Michal Moskal, Jonathan de Halleux, and Manuel Fahndrich
Play with RiSE tools at www.rise4fun.com Sources Dafny: a verification-oriented programming language CCI: Common compiler infrastructure
Downloads Z3: an automated theorem prover
Pex: parameterized unit testing Boogie language/tool for program verification tools
Automata: symbolic automata F*: verification of functional programs Code contracts CHESS: systematic concurrency testing
Advanced graph layout VCC: verification of concurrent C programs
Play with RiSE tools at www.rise4fun.com
Dafny: a verification-oriented programming language
CCI: Common compiler infrastructure
The RiSE team consists of 30+ passionate researchers and developers.
- 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.
- 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.
- 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.
- 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.
- Christopher Theisen, Kim Herzig, Patrick Morrison, Brendan Murphy, and Laurie Williams, Approximating Attack Surfaces with Stack Traces, in Companion Proceedings of the 37th International Conference on Software Engineering, IEEE – Institute of Electrical and Electronics Engineers, May 2015.
- Thomas Ball, Sebastian Burckhardt, Jonathan de Halleux, Michał Moskal, Jonathan Protzenko, and Nikolai Tillmann, Beyond Open Source: The TouchDevelop Cloud-based Integrated Development Environment, in In Proceedings of 2nd ACM International Conference on Mobile Software Engineering and Systems (MOBILESoft), ACM – Association for Computing Machinery, May 2015.
- Michael Barnett, Christian Bird, Joao Brunet, and Shuvendu Lahiri, Helping developers help themselves: Automatic decomposition of code review changesets., in Proceedings of the 37th International Conference on Software Engineering, IEEE – Institute of Electrical and Electronics Engineers, May 2015.
- Kim Herzig and Nachiappan Nagappan, Empirically Detecting False Test Alarms Using Association Rules, in Companion Proceedings of the 37th International Conference on Software Engineering, IEEE – Institute of Electrical and Electronics Engineers, May 2015.
- Na Meng, Lisa Hua, Miryung Kim, and Kathryn S. McKinley, Does Automated Refactoring Obviate Systematic Editing?, ACM – Association for Computing Machinery, May 2015.
- Jonathan Mace, Peter Bodik, Rodrigo Fonseca, and Madanlal Musuvathi, Retro: Targeted Resource Management in Multi-tenant Distributed Systems, in NSDI, May 2015.
- Kim Herzig, Michaela Greiler, Jacek Czerwonka, and Brendan Murphy, The Art of Testing Less without Sacrificing Quality, in Proceedings of the 2015 International Conference on Software Engineering, IEEE – Institute of Electrical and Electronics Engineers, May 2015.
- Miryung Kim, Thomas Zimmermann, Robert DeLine, and Andrew Begel, The Emerging Role of Data Scientists on Software Development Teams, no. MSR-TR-2015-30, 12 April 2015.
- Abram Hindle, Christian Bird, Thomas Zimmermann, and Nachiappan Nagappan, Do Topics Make Sense to Managers and Developers?, in Empirical Software Engineering, vol. 20, no. 2, pp. 479-515, Springer, April 2015.
- Patrick Morrison, Kim Herzig, Brendan Murphy, and Laurie Williams, Challenges with Applying Vulnerability Prediction Models, in Proceedings of the 2015 Symposium and Bootcamp on the Science of Security, ACM – Association for Computing Machinery, April 2015.
- Arvind Haran, Montgomery Carter, Michael Emmi, Akash Lal, Shaz Qadeer, and Zvonimir Rakamaric, SMACK+Corral: A Modular Verifier (Competition Contribution), in Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Springer, March 2015.
- Margus Veanes and Nikolaj Bjørner, Symbolic Tree Automata, in Information Processing Letters, vol. 115, no. 3, pp. 418-424, Elsevier, March 2015.
- E. Haque, Yong hun Eom, Yuxiong He, Sameh Elnikety, Ricardo Bianchini, and Kathryn S. McKinley, Few-to-Many: Incremental Parallelism for Reducing Tail Latency in Interactive Services, ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), March 2015.
- Margus Veanes, Symbolic String Transformations with Regular Lookahead and Rollback, in PSI 2014, Springer Verlag, February 2015.
- Emerson Murphy-Hill, Thomas Zimmermann, Christian Bird, and Nachiappan Nagappan, The Design Space of Bug Fixes and How Developers Navigate It, in IEEE Transactions on Software Engineering, vol. 41, no. 1, pp. 65-81, IEEE – Institute of Electrical and Electronics Engineers, January 2015.
- Margus Veanes, Todd Mytkowicz, David Molnar, and Benjamin Livshits, Data-Parallel String-Manipulating Programs, in POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM – Association for Computing Machinery, January 2015.
- Sebastian Burckhardt, Daan Leijen, Jonathan Protzenko, and Manuel Fähndrich, Global Sequence Protocol: A Robust Abstraction for Replicated Shared State (Extended version), no. MSR-TR-2015-11, 1 January 2015.
Try a Coding Duel at www.pexforfun.com
- Microsoft Researchers on 2013 ICFP Competition
- Peter Heldens - Creating Scripts with TouchDevelop
- TouchDevelop - Getting Started
- Guido de Caso - Distributed Knowledge Authorization Language
- ICSE 2011: Conversation with Baris Aktemur
- ICSE 2011: Danny Dig - Retrofitting Parallelism into a Sequential World
- ICSE 2011: Dieter Rombach - Software Engineering Process Methodology