31 January 2019 – Associate Professor Ilya Sergey and his collaborator, University of California San Diego Assistant Professor Nadia Polikarpova, received the Distinguished Paper Award at the 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019), held from 13 to 19 January 2019 in Cascais, Portugal.
POPL is a flagship conference on all aspects of programming languages and programming systems. It promotes both theoretical and experimental results, on topics ranging from formal frameworks to experience reports. A total of 77 papers out of 267 were accepted to the conference, with six papers receiving the Distinguished Paper Award.
A/P Sergey, who holds a joint appointment with NUS Computing and Yale-NUS College, won the coveted award for his paper on synthesising imperative programmes with pointers. Programme synthesis is a subfield in Computer Science whereby programmes are automatically constructed based on given specifications set by the programmer.
“Synthesising a correct programme is very similar to writing a rigorous mathematical proof in traditional mathematical theorems,” said A/P Sergey. In mathematics, a proof show that the result of the theorem is true. In the same way, a proof can also be generated to demonstrate that a programme meets its desired conditions. A/P Sergey believes that this technique of verifying the accuracy of programmes can also be used to synthesise them. “Proofs follow a certain logic. In this research, we are able to use logic and the programme specifications to generate a programme and a proof that follows the logic used,” A/P Sergey added.
The paper, “Structuring the Synthesis of Heap-Manipulating Programs”, proposed to use Separation Logic, a state-of-the-art formal framework for industry-scale programme analysis, to drive programme synthesis. Programmers will only need to write the programme’s desired pre- and postconditions, and a corresponding programme will be generated automatically. “Not only do you get a programme that meets the desired specifications, you will also get a formal proof that it does so,” explained A/P Sergey.
The team implemented this novel idea in a tool, called SuSLik, which has been used to synthesise a variety of programmes, ranging from data structure destructors to complex container transformations. The pair also managed to obtain the synthesis algorithm, which is able to synthesise programmes faster than other existing approaches. “Most of the interesting programmes we synthesised were done in within a second,” said A/P Sergey.
“We believe that our discovery about the tight relation between Separation Logic and programme synthesis opens new exciting directions for theoretical research in programme logics. At the same time, we were pleasantly surprised by the performance of our synthesis tool, and we look forward to explore its applications,” A/P Sergey added.
