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.
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:
|
Browser/JavaScript |
||
|
New Ways to Program |
||
|
Modeling and Design |
||
|
Contracts and Types |
||
|
Verification |
||
|
Symbolic Methods |
Automata, BEK, Duality, Rex, SymDiff, Z3 | |
|
Testing |
||
|
Runtime Reliability |
||
|
Performance |
||
|
Concurrency & Parallelism |
||
|
Measurement and Prediction |
||
|
User Studies |
Games | |
|
Critical Technologies |
Research Overviews
- Looking Back on the Language and Hardware Revolutions: Measured Power, Performance, and Scaling, H. Esmaeilzadeh, T. Cao, X. Yang, S. M. Blackburn, and K. S. McKinley, ASPLOS 2011
- Empirical Software Engineering at Microsoft Research, C. Bird, B. Murphy, N. Nagappan, and T. Zimmermann, CSCW 2011
- SAGE: Whitebox Fuzzing for Security Testing, P. Godefroid, M. Y. Levin, D. Molnar, ACM Queue 2012
- Satisfiability Modulo Theories: Introduction and Applications, Leonardo De Moura, Nikolaj Bjørner, CACM 2011
- Specification and Verification: The Spec# Experience, M. Barnett, M. Fähndrich, K. R. M. Leino, P. Müller, W. Schulte, H. Venter, CACM 2011
- A Decade of Software Model Checking with SLAM, T. Ball, V. Levin, S. K. Rajamani, CACM 2011
- Microsoft's Protocol Documentation Program: Interoperability Testing at Scale, A discussion with N. Kicillof, W. Grieskamp, and B. Binder (work based on SpecExplorer). CACM 2011
- Predictable and Progressive Testing of Multithreaded Code, T. Ball, S. Burckhardt, P. de Halleux, M. Musuvathi, S. Qadeer, IEEE Software 2011
Publications
2012
- Sebastian Burckhardt, Manuel Fahndrich, Daan Leijen, and Mooly Sagiv, Eventually Consistent Transactions, in Proceedings of the 22n European Symposium on Programming (ESOP), Springer, 24 March 2012
- Margus Veanes and Nikolaj Bjorner, Symbolic Automata: The Toolkit, in TACAS'12, Springer Verlag, March 2012
- Thomas Zimmermann and Christian Bird, Collaborative Software Development in Ten Years: Diversity, Tools, and Remix Culture, in Proceedings of the CSCW Workshop on the Future of Collaborative Software Development (FutureCSD 2012), ACM, February 2012
- K. Rustan M. Leino and Aleksandar Milicevic, Program Extrapolation with Jennisys, no. MSR-TR-2012-12, February 2012
- Miryung Kim, Thomas Zimmermann, and Nachiappan Nagappan, Appendix to A Field Study of Refactoring Rationale, Benefits, and Challenges at Microsoft, no. MSR-TR-2012-4, 11 January 2012
- Pierre-Yves Strub, Nikhil Swamy, Cedric Fournet, and Juan Chen, Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq, in In Proceedings of the ACM Symposium on Principles on Programming Languages, ACM, January 2012
- Saurabh Joshi, Shuvendu Lahiri, and Akash Lal, Underspecified Harnesses and Interleaved Bugs, in Principles of Programming Languages (POPL) 2012, ACM SIGPLAN, January 2012
- Francesco Logozzo, Our Experience with the CodeContracts Static Checker, in Proceedings of the Verified Software: Theories, Tools, and Experiments, Springer, January 2012
- Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, and Nikolaj Bjorner, Symbolic Finite State Transducers: Algorithms and Applications, in POPL’12, ACM SIGPLAN, January 2012
- Akash Lal, Shaz Qadeer, and Shuvendu Lahiri, Corral: A Solver for Reachability Modulo Theories, no. MSR-TR-2012-9, January 2012
2011
- Ashish Gupta, Thomas Zimmermann, Christian Bird, Nachiappan Nagappan, Thirumalesh Bhat, and Syed Emran, Detecting Energy Patterns in Software Development, no. MSR-TR-2011-106, 16 November 2011
- Margus Veanes, David Molnar, Benjamin Livshits, and Lubomir Litchev, Generating Fast String Manipulating Code Through Transducer Exploration and SIMD Integration, no. MSR-TR-2011-124, November 2011
- Margus Veanes and Nikolaj Bjorner, Alternating simulation and IOCO, in International Journal on Software Tools for Technology Transfer (STTT) , Springer, November 2011
- Tim Menzies, Andrew Butcher, Andrian Marcus, and Thomas Zimmermann, Local vs Global Models for Effort Estimation and Defect Prediction, in Proceedings of the 26st IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), IEEE, November 2011
- Kenneth L. McMillan, Interpolants from Z3 proofs, in Formal Methods in Computer-Aided Design, 30 October 2011
- Clemens Kolbitsch, Benjamin Livshits, Benjamin Zorn, and Christian Seifert, Rozzle: De-Cloaking Internet Malware, no. MSR-TR-2011-94, 25 October 2011
- Sebastian Burckhardt, Daan Leijen, Caitlin Sadowski, Jaeheon Yi, and Thomas Ball, Two for the Price of One: A Model for Parallel and Incremental Computation, in Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'11), ACM SIGPLAN, Portland, Oregon, 22 October 2011
- Sebastian Burckhardt, Manuel Fahndrich, Daan Leijen, and Mooly Sagiv, Eventually Consistent Transactions (full version), no. MSR-TR-2011-117, October 2011
- Chris Hawblitzel, Ming Kawaguchi, Shuvendu Lahiri, and Henrique Rebelo, Mutual summaries and relative termination, no. MSR-TR-2011-112, October 2011
- Marat Akhin, Nikolai Tillmann, Manuel Fahndrich, Jonathan de Halleux, and Michal Moskal, Code Similarity in TouchDevelop: Harnessing Clones, no. MSR-TR-2011-103, 9 September 2011
- Manuel Fahndrich and Francesco Logozzo, Checking Compatibility of Bit Sizes in Floating Point Comparison Operations, in Proceedings of the 3rd workshop on Numerical and Symbolic Abstract Domains, Electronic Proceedings in Theoretical Computer Science, September 2011
- Andreas Zeller, Thomas Zimmermann, and Christian Bird, Failure is a Four-Letter Word: A Parody in Empirical Research, in Proceedings of the 7th International Conference on Predictive Models in Software Engineering, ACM, September 2011
- Ayse Tosun Misirli, Brendan Murphy, Thomas Zimmermann, and Ayse Basar, An Explanatory Analysis on Eclipse Beta-Release Bugs Through In-Process Metrics, in Proceedings of the 8th International Workshop on Software Quality (WoSQ 2011), ACM, September 2011
- Nikhil Swamy, Juan Chen, Cedric Fournet, Pierre-Yves Strub, Karthikeyan Bharagavan, and Jean Yang, Secure Distributed Programming with Value-dependent Types, in The 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011), ACM SIGPLAN, September 2011
- Alexander Tarvo, Thomas Zimmermann, and Jacek Czerwonka, An Integration Resolution Algorithm for Mining Multiple Branches in Version Control Systems (Industry Track), in Proceedings of the 27th IEEE International Conference on Software Maintenance (ICSM 2011), IEEE, September 2011
Links

Try a Coding Duel at www.pexforfun.com
Try our tools!
RiSE @ Channel9
- 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
- ICSE 2011: Grigore Rosu - The Art and Science of Program Verification




