Yale-NUS Computer Science Professor wins POPL 2019 Distinguished Paper Award
Associate Professor Ilya Sergey won a Distinguished Paper Award at the POPL conference in January. Image by Yale-NUS College.
Yale-NUS faculty are making a name for themselves on the international stage, proving that this small liberal arts college punches above its weight in the academic arena.
Associate Professor of Science (Computer Science) Ilya Sergey, who holds a joint appointment with Yale-NUS and the National University of Singapore (NUS) School of Computing, received the Distinguished Paper Award at the 46th Association for Computing Machinery’s Special Interest Group on Programming Languages (ACM SIGPLAN) Symposium on Principles of Programming Languages (POPL 2019), along with his co-author, Assistant Professor Nadia Polikarpova of the University of California, San Diego.
POPL is an annual academic conference on all aspects of programming languages and programming systems. This year’s conference was held from 13 to 19 January in Cascais, Portugal. All papers accepted to the conference had to pass a rigorous two-phase peer reviewing process, and were published in the ACM Journal on Programming Languages.
A total of 77 papers out of 267 submissions were accepted to the conference, with six papers – of which Assoc Prof Sergey’s was one – receiving the Distinguished Paper Award.
Assoc Prof Sergey and Asst Prof Polikarpova’s paper, entitled ‘Structuring the Synthesis of Heap-Manipulating Programs’, leveraged the tight relationship between synthesising a program and writing rigorous mathematical proofs to create a new tool to synthesise programs.
Program synthesis is the process of automatically constructing a program that satisfies a given specification. Assoc Prof Sergey and Asst Prof Polikarpova used Separation Logic, a popular formal reasoning framework, to define the program synthesis procedure as a proof search.
In mathematics, proofs are used to demonstrate that the result from a given theorem is true. Similarly, proofs are used in programming to demonstrate that a given program works according to its specifications.
“Synthesising a correct program is very similar to writing a rigorous mathematical proof in traditional mathematical theorems,” said Assoc Prof Sergey. “Proofs follow a certain logic. In this research, we are able to use logic and the program specifications to generate a program and a proof that follows the logic used.”
Using formal logic methods, Assoc Prof Sergey and Asst Prof Polikarpova were able to create a tool to synthesise programs. This tool, called SuSLik, was able to produce programs within less than a second, improving by more than an order of magnitude on the performance of existing state-of-the-art tools for program synthesis.
SuSLik can not only generate a program that fits desired specifications, it also produces a formal proof that the program does in fact fit those specifications.
“We believe that our discovery about the tight relation between Separation Logic and programme synthesis opens new exciting directions for theoretical research in program logics. At the same time, we were pleasantly surprised by the performance of our synthesis tool, and we look forward to explore its applications,” Assoc Prof Sergey said.
In addition to his award-winning paper, Assoc Prof Sergey also presented a paper on provably correct static race detection at POPL, co-authored with two collaborators, Dr Nikos Gorogiannis (Middlesex University London) and Professor Peter O’Hearn (University College London). The paper discussed ahead-of-time detection of bugs in concurrent code (such as what is run on modern parallel processors), showing how these bugs can be caught before the possibly affected software is even deployed.
The main theme of Assoc Prof Sergey’s research is construction and formal verification of software in which correctness is critical; this focuses on creating software that performs according to a given set of specifications, and demonstrating that the software works via formal proofs.
This theme is currently being integrated into the Mathematical, Computational and Statistical Sciences courses he is teaching at Yale-NUS, such as Introductory Data Structures and Algorithms. Assoc Prof Sergey also plans to use this research topic as a ground for future capstone and internship projects.
