Programming languages and software engineering research area
Return to Microsoft Research Lab – Redmond

Research in Software Engineering (RiSE)

新闻与深度文章

Microsoft Research Focus 03: Week of November 7th, 2022
微软研究院博客

Welcome to Research Focus, a new series …

奖项 | TOGA: A Neural Method for Test Oracle Generation

ICSE’22 ACM SIGSOFT Distinguished Paper Award 

An illustration of resolving a bad merge into a safe merge. Moving from left to right, circles on a continuous line represent code commits in a version control system. A circle labeled “Base” is the most common ancestor of the commits marked A and B, respectively. All three commits pass the project’s quality gates, denoted by green check marks alongside each of these commits. The subsequent merge results in a failure of some quality gate, denoted by a blue circle labeled “Bad merge” with a red x above it. The repair uses machine learning, denoted by an abstract image of a neural network, and program verification and synthesis, denoted by a formal inference rule containing math symbols, to construct a safe merge that passes the quality gate, denoted by a circle outlined in green with a green check mark above it.   
微软研究院博客

| Shuvendu Lahiri

Since the computing world began embracin…

奖项 | PLDI 2021 Conference

Ben Zorn awarded SIGPLAN Distinguished Service Award 2021 

Ben Zorn was honored with the SIGPLAN Di…

An animation showing an example of a high-level language message format specified by EverParse. From the message, two arrows labeled “EverParse” point to a rectangle labeled “formal specification” and a rectangle labeled “low-level implementation,” respectively, inside a larger rectangle labeled “F* code.” The figure represents EverParse’s ability to automatically generate safe, correct, and fast F* parsing code. “Correctness” is defined as “Correctness: ​parse (serialize msg) = msg​” and “valid msg ==> serialize (parse msg) = msg​.” The F* logo appears with the description that F* is a type theory–based programming language and proof assistant that can prove theorems about programs​. From the “F* code” rectangle, arrows point from the “low-level implementation” rectangle and a rectangle labeled “verified libraries for combinators” to a rectangle labeled “Safe high-performance C code.”
微软研究院博客

| Tahina Ramananandro, Aseem Rastogi, 和 Nikhil Swamy

EverParse (opens in new tab) is a framew…

Diagram explaining RESTler API fuzzing tool
微软研究院博客

Cloud services have become the new criti…

新闻报道 | MSPoweruser

Microsoft Research announce TileCode, a game creation app that can run on handhelds 

Microsoft Research has announced a new p…

Dr. Ant Rowstron and Mark Russinovich on the Microsoft Research podcast
微软研究院播客

Computer programming has often been perc…

a screen shot of a computer
微软研究院博客

| Michal Moskal

When we began developing Microsoft MakeC…