{"id":144812,"date":"2008-11-24T00:13:15","date_gmt":"2008-11-24T00:13:15","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/group\/research-in-software-engineering-rise\/"},"modified":"2025-11-21T11:00:11","modified_gmt":"2025-11-21T19:00:11","slug":"research-software-engineering-rise","status":"publish","type":"msr-group","link":"https:\/\/www.microsoft.com\/en-us\/research\/group\/research-software-engineering-rise\/","title":{"rendered":"Research in Software Engineering (RiSE)"},"content":{"rendered":"
\n\t
\n\t\t
\n\t\t\t\"Programming\t\t<\/div>\n\t\t\n\t\t
\n\t\t\t\n\t\t\t
\n\t\t\t\t\n\t\t\t\t
\n\t\t\t\t\t\n\t\t\t\t\t
\n\t\t\t\t\t\t
\n\t\t\t\t\t\t\t\t\t\t\t\t\t\t\t\n\t\t\t\t\t\t\t\t\t<\/span>\n\t\t\t\t\t\t\t\t\tReturn to Microsoft Research Lab – Redmond\t\t\t\t\t\t\t\t<\/a>\n\t\t\t\t\t\t\t\n\t\t\t\t\t\t\t\n\n

Research in Software Engineering (RiSE)<\/h1>\n\n\t\t\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t<\/div>\n\t<\/div>\n<\/section>\n\n\n\n\n\n
\"Research<\/figure>\n\n\n\n

The RiSE group builds the system and foundations of programming through open-ended fundamental research in formal methods, high-performance computing, programming languages, and software engineering. We collectively work towards a future where computing systems are provably correct, secure, and performant. Our research synergistically combines symbolic reasoning, AI, and human-centric methods to empower every programmer and organization to achieve more. <\/p>\n\n\n\n

Our research falls into the following thrusts: <\/p>\n\n\n\n

Natural Specifications<\/h5>\n\n\n\n

We believe that future programming systems will allow humans to specify their intent naturally with the computer distilling this intent interactively into a precise formal specification. Towards this end, we are conducting research in the intersection of formal reasoning and natural-language processing to synthesize specifications from several natural artefacts: documentation, code, runtime traces, etc.<\/p>\n\n\n\n

TAPP<\/a>, TiCoder<\/a>, TOGA<\/a>, NL2Post<\/a>, 3DGen (opens in new tab)<\/span><\/a>, Prompts are Programs (opens in new tab)<\/span><\/a> <\/p>\n\n\n\n

Verified Programming<\/h5>\n\n\n\n

Over the past decade, we have made huge strides in developing proof-oriented programming methodologies for building provably correct systems. For instance, verified parsers from our group now validates every packet in Azure to provably eliminate entire classes of security vulnerabilities. We are using AI advances to significantly increase the scope of proof-oriented programming and accelerate the development of provably correct systems. <\/p>\n\n\n\n

Project Everest<\/a>, EverParse (opens in new tab)<\/span><\/a>, AutoParse, Verus, Pulse, Kuiper<\/p>\n\n\n\n

Verified Configurations<\/h5>\n\n\n\n

Correctness of systems crucially depends on their configurations; misconfigurations, as equally as program bugs, can lead to serious reliability and security issues. We have long used symbolic reasoning methods to detect configuration errors in production systems; for instance, Azure makes more than 5 billion calls to our configuration verification tool every day and generates tens to thousand alerts that would otherwise could result in serious outages. We are developing methods to automatically infer intent to accelerate the verification of configurations. <\/p>\n\n\n\n

Network Verification<\/a><\/p>\n\n\n\n

High-Performance Computing & AI Infrastructure<\/h5>\n\n\n\n

We are developing state-of-the art high-performance computing and compiler techniques to improve the performance of our AI infrastructure. Programming abstractions and high-performance kernels developed by our group are used to serve production AI workloads in Azure. <\/p>\n\n\n\n

MSCCL (opens in new tab)<\/span><\/a>, MSCCL++ (opens in new tab)<\/span><\/a>, CuSync (opens in new tab)<\/span><\/a>, FastKron (opens in new tab)<\/span><\/a>, TritonComm, Guidance (opens in new tab)<\/span><\/a><\/p>\n\n\n\n

Formal Methods & Automated Reasoning<\/h5>\n\n\n\n

Our research is firmly rooted in formally reasoning about the correctness and performance of systems. To this end, we invest in long-term foundational research in formal methods and automated reasoning. <\/p>\n\n\n\n

Lean (opens in new tab)<\/span><\/a>, Symbolic Automata<\/a>, Z3<\/a> <\/p>\n\n\n\n

Programming Languages & Systems<\/h5>\n\n\n\n

We develop core programming language abstractions to improve the productivity of programmers everywhere. <\/p>\n\n\n\n

F* (opens in new tab)<\/span><\/a>, Koka (opens in new tab)<\/span><\/a>, Azure Durable Functions (opens in new tab)<\/span><\/a>, Netherite (opens in new tab)<\/span><\/a>, Orleans<\/a>, Microsoft MakeCode<\/a>, Jacdac (opens in new tab)<\/span><\/a>, MSAGL-JS (opens in new tab)<\/span><\/a>, GenAIScript (opens in new tab)<\/span><\/a><\/p>\n\n\n\n

\n
Connect on Twitter<\/a><\/div>\n<\/div>\n\n\n\n\n\n

<\/p>\n","protected":false},"excerpt":{"rendered":"

RiSE coordinates Microsoft\u2019s 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\u2019s businesses.<\/p>\n","protected":false},"featured_media":498053,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr_group_start":"","footnotes":""},"research-area":[13556,13554,13560,13558],"msr-group-type":[243694],"msr-locale":[268875],"msr-impact-theme":[],"class_list":["post-144812","msr-group","type-msr-group","status-publish","has-post-thumbnail","hentry","msr-research-area-artificial-intelligence","msr-research-area-human-computer-interaction","msr-research-area-programming-languages-software-engineering","msr-research-area-security-privacy-cryptography","msr-group-type-group","msr-locale-en_us"],"msr_group_start":"","msr_detailed_description":"","msr_further_details":"","msr_hero_images":[],"msr_research_lab":[199565],"related-researchers":[{"type":"user_nicename","display_name":"Shraddha Barke","user_id":43605,"people_section":"Group 1","alias":"sbarke"},{"type":"user_nicename","display_name":"Nikolaj Bj\u00f8rner","user_id":33067,"people_section":"Group 1","alias":"nbjorner"},{"type":"user_nicename","display_name":"Sebastian Burckhardt","user_id":33544,"people_section":"Group 1","alias":"sburckha"},{"type":"user_nicename","display_name":"Saikat Chakraborty","user_id":42411,"people_section":"Group 1","alias":"saikatc"},{"type":"user_nicename","display_name":"Shuo Chen","user_id":33637,"people_section":"Group 1","alias":"shuochen"},{"type":"user_nicename","display_name":"Gabriel Ebner","user_id":42573,"people_section":"Group 1","alias":"gabrielebner"},{"type":"user_nicename","display_name":"Sarah Fakhoury","user_id":42180,"people_section":"Group 1","alias":"sfakhoury"},{"type":"user_nicename","display_name":"Cormac Herley","user_id":31468,"people_section":"Group 1","alias":"cormac"},{"type":"user_nicename","display_name":"Abhinav Jangda","user_id":42438,"people_section":"Group 1","alias":"ajangda"},{"type":"user_nicename","display_name":"Shuvendu Lahiri","user_id":33640,"people_section":"Group 1","alias":"shuvendu"},{"type":"user_nicename","display_name":"Daan Leijen","user_id":31497,"people_section":"Group 1","alias":"daan"},{"type":"user_nicename","display_name":"Guido Mart\u00ednez","user_id":42915,"people_section":"Group 1","alias":"guimartinez"},{"type":"user_nicename","display_name":"Angelica Moreira","user_id":43167,"people_section":"Group 1","alias":"anmoreira"},{"type":"user_nicename","display_name":"Madan Musuvathi","user_id":32766,"people_section":"Group 1","alias":"madanm"},{"type":"user_nicename","display_name":"Lev Nachmanson","user_id":32653,"people_section":"Group 1","alias":"levnach"},{"type":"user_nicename","display_name":"Tahina Ramananandro","user_id":36293,"people_section":"Group 1","alias":"taramana"},{"type":"user_nicename","display_name":"Aashaka Shah","user_id":43056,"people_section":"Group 1","alias":"aashakashah"},{"type":"user_nicename","display_name":"Nikhil Swamy","user_id":33138,"people_section":"Group 1","alias":"nswamy"},{"type":"user_nicename","display_name":"Margus Veanes","user_id":32806,"people_section":"Group 1","alias":"margus"},{"type":"user_nicename","display_name":"Ben Zorn","user_id":35154,"people_section":"Group 1","alias":"zorn"},{"type":"user_nicename","display_name":"Peli de Halleux","user_id":32253,"people_section":"Group 1","alias":"jhalleux"}],"related-publications":[544248,547563,547581,544029,505508,498287,498272,481464,509975,343232,317378,337556,331022,327005,293297,300014,311420,293159,295586,292055,238212,277953,276159,265746,262947,259824,238227,251183,238213,242537,240029,237713,238009,238008,238253,238011,238255,268689,238033,238211,251192,238360,342335,238210,342380,215040,238214,238358,168897,238242,168680,342575,168866,168251,238216,168588,168606,238209,342365,168608,168309,168312,167947,167911,168444,168409,167912,168311,167952,168002,167910,168192,238254,168252,167985,167511,168310,167848,167962,166496,167997,167641,238359,167494,167966,167640,342341,342356,167744,167718,167717,167135,167509,167601,215211,167075,167514,167125,167510,166823,166766,167039,166655,166431,166434,166342,268665,166184,166341,166495,166407,166172,166362,166673,166488,166474,166343,166526,166535,166405,166327,166117,166116,166332,166331,166118,165601,166062,166131,165602,165785,165887,165882,165514,165795,165734,165581,165482,165218,165455,165458,164902,164869,164903,164709,165248,165174,238222,165492,164733,268680,164713,342458,165197,164665,342617,268593,342974,165473,342473,238224,238207,268587,342482,238223,342497,343076,342629,345005,344987,344999,344960,344969,344927,345035,345029,345017,345011,342044,342395,342050,342056,342062,342077,342083,342089,342125,345050,345044,342137,343088,268656,343118,343340,268581,345083,268671,342743,342635,268572,153101,343283,343349,343289,343304,343358,343313,344918,564462,568212,569658,569919,569985,569997,570141,571362,571410,578803,579268,590623,594865,605844,606792,606990,611871,613197,616287,617616,617628,617634,618528,619023,622893,627912,640638,640647,642384,647484,671025,671076,671754,674928,683523,683847,684834,690579,695655,698899,701437,705892,707329,710158,724828,731026,732448,732454,738607,739885,746071,750325,751681,756349,761113,764872,765124,769738,771451,774058,782968,794180,798427,805813,815425,841948,841975,845653,860862,860991,863379,864348,864888,879321,879978,885843,890070,900717,900732,901725,910749,913911,925401,933960,936282,936297,939696,953625,953640,953652,954237,955017,965088,976782,976788,978444,981003,982593,1029975,1030137,1039380,1039398,1041069,1057761,1057767,1084344,1085355,1087500,1092855,1094508,1113288,1115505,1115514,1115526,1139401,1140366,1140375,1141099,1146073,1149341,1151931,1156515,1159286,1160973,1161825,1168713],"related-downloads":[],"related-videos":[186544,186687,186689,186691,186701,186703,186711,186721,186765,186882,186930,186944,186953,186955,186957,186983,187121,187125,187167,187271,187346,187380,187501,187509,187511,187529,187562,187580,187625,187629,187649,187701,187703,187743,188072,188076,188090,188170,188172,188174,188182,188205,188259,188419,188425,188433,188434,188462,188464,188466,188468,188470,188472,188474,188480,188482,188484,188486,188514,188601,188672,188773,188825,188852,189062,189110,189160,189182,189226,189236,189246,189325,189345,189368,189370,189446,189464,189518,189532,189534,189546,189622,189656,189762,189806,189880,189890,189962,189994,190067,190130,190136,190209,190211,190317,190345,190392,190523,190625,190648,190656,190699,190707,190719,190783,190874,191469,191600,191606,191620,214987,215001,215014,264708,488528,492101,492395,492413,494207,490616,508007,590323,603921,608070,608364,612873,616533,695958,748933,749422,798052,843973,843994],"related-projects":[890049,807097,795815,879960,649749,235367,642720,590746,579283,554055,504254,427296,212086,259698,171471,325037,171416,292964,171153,171010,170993,170943,170698,170570,170573,825511],"related-events":[200055,199971,199951,199792,199735],"related-opportunities":[1150730,1162689],"related-posts":[4241,5501,306476,307343,359282,384782,432156,456975,465990,476433,496727,557352,559317,570825,588916,589363,1163539,1135033,1124682,1102680,1044072,1032900,1029624,984711,895428,765556,734818,705790,620664,605124,602154,3651],"tab-content":[{"id":0,"name":"In the news","content":"Ben Zorn and Tom Ball hosted the Pacific Northwest Programming Languages and Software Engineering workshop<\/a> at Microsoft Research Redmond in Building 99 on May 14, 2018.\r\n\r\nMicrosoft Research received the 2016 IEEE Technical Council on Software Engineering (TCSE) Distinguished Synergy Award<\/a> \u201cpresented 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.\u201d\r\n\r\nCRA Women Celebrates Women\u2019s History Month<\/a> features interview with Kathryn McKinley\r\n\r\nProject Premonition<\/a> aims to use mosquitoes, drones, cloud computing to prevent disease outbreaks\u00a0 [video<\/a>]\u00a0 [article<\/a>]"},{"id":1,"name":"Awards","content":"

\r\n

2017<\/h3>\r\nSkolem Award<\/strong><\/a> - CADE-21 (2007): Leonardo de Moura and Nikolaj Bj\u00f8rner<\/em> - Efficient E-Matching for SMT Solvers<\/strong>\r\n

2016<\/h3>\r\nMining Software Repositories' 2016 Most Influential Paper Award <\/strong>for\u00a0Mining Email Social Networks<\/em> by Christian Bird<\/a>, Alex Gourley, Prem Devanbu, Michael Gertz, Anand Swaminathan\r\n\r\nICSE 2016 Distinguished Paper Award <\/strong>for Guiding Dynamic Symbolic Execution Toward Unverified Program Executions by Maria Christakis<\/a> and co-authors\r\n\r\nMaria Christakis<\/a>'s\u00a0Ph.D. thesis was nominated by ETH for the Gesellschaft f\u00fcr Informatik prize for best dissertation<\/strong>\r\n

2015<\/h3>\r\nESEC\/FSE 2015 Distinguished Paper, <\/strong>How Practitioners Perceive the Relevance of Software Engineering Research, David Lo, Nachi Nagappan<\/a>, Thomas Zimmermann<\/a>\r\n\r\nSIGPLAN Research Highlight (May 2015), <\/strong>Parallelizing dynamic programming through rank convergence<\/a>, Saeed Maleki, Madanlal Musuvathi<\/a>,\u00a0 Todd Mytkowicz<\/a>\r\n\r\nNachi Nagappan<\/a> named a 2015 ACM Distinguished Scientist<\/strong>\r\n\r\nThe 2015 ACM Programming Languages Software Award<\/strong> goes to Christoph Wintersteiger<\/a>, Leonardo de Moura<\/a>, and Nikolaj Bjorner<\/a> of MSR for their foundational work on the Z3 automated theorem prover<\/a>, which powers several generations of testing, analysis and verification tools.\r\n\r\nGuiness Book of World Records<\/strong>: The most people trained in computer programming in 8<\/a> 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<\/a>)\r\n\r\nSIGPLAN PLDI 2015 Distinguished Artifact Award, <\/strong>FlashRelate: extracting relational data from semi-structured spreadsheets using examples<\/a>, Daniel W. Barowy<\/a>, Sumit Gulwani, Ted Hart, and Benjamin Zorn<\/a>\r\n

2014<\/h3>\r\n2014 CAV Award \"<\/strong>For the development of partial-order reduction algorithms for efficient state-space exploration of concurrent systems\", Patrice Godefroid<\/a>, Doron Peled, Antti Valmari, Pierre Wolper\r\n\r\nICSE 2014 Most Influential Paper Award<\/strong>, Mining Version Histories to Guide Software Changes, Thomas Zimmermann<\/a>,\u00a0Peter Weissgerber, Stephan Diehl and Andreas Zeller\r\n\r\n\"Uncertain<T>: A First-Order Type for Uncertain Data,\" J. Bornholt, T. Mytkowicz<\/a>, and K.S. McKinley, ASPLOS 2014, selected for ACM SIGPLAN Research Highlights<\/strong>, November 2014.\r\n\r\nFMCAD Best Paper Award<\/strong>. Akash Lal and Shaz Qadeer<\/a>, A Program Transformation for Faster Goal-Directed Search<\/a>, in Formal Methods in Computer-Aided Design (FMCAD)<\/em>, FMCAD, October 2014.\r\n\r\n2014 ACM SIGMETRICS Test of Time Award<\/strong>, for Kathryn McKinley's<\/a> paper \u201cMyths and Realities: The Performance Impact of Garbage Collection\u201d co-authored with Steve Blackburn and Perry Cheng which appeared originally in SIGMETRICS June 2004.\r\n\r\nFSE 2014 Distinguished Paper: <\/strong>Miltiadis Allamanis, Earl T. Barr, Christian Bird<\/a>, and Charles Sutton, Learning Natural Coding Conventions<\/a>\r\n\r\nFSE 2014 Distinguished Paper<\/strong>: Akask Lal, Shaz Qadeer<\/a>, Powering the Static Driver Verifier using Corral<\/a>\r\n\r\n<\/div>"}],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-group\/144812","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-group"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-group"}],"version-history":[{"count":77,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-group\/144812\/revisions"}],"predecessor-version":[{"id":1156250,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-group\/144812\/revisions\/1156250"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/498053"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=144812"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=144812"},{"taxonomy":"msr-group-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-group-type?post=144812"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=144812"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=144812"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}