11 June 2021 – NUS Computing and Yale-NUS College Associate Professor Ilya Sergey has won the Distinguished Paper Award from the 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation conference.
The award was given to only eight out of 87 papers accepted for the conference, which is scheduled to be held online from 20 to 26 June 2021.
A/P Sergey and his research collaborators received the award for their paper, Cyclic Program Synthesis, which describes a new deductive program synthesis technique that uses cyclic proofs — a reasoning mechanism from automated theorem proving.
This new methodology can synthesise heap-manipulating programs that rely on arbitrary auxiliary recursive procedures.
“Our technique is capable of automatically discovering recursive auxiliaries without the need for built-in templates, or additional hints from the user. This solves a long-standing challenge that has been beyond the reach for existing program synthesis approaches,” said A/P Sergey.
The new methodology has been implemented in Cypress, a new synthesis tool developed by the team that is publicly available online.
It automates generation of programs for an important class of tasks that occur routinely in transformations of complex linked data structures (e.g., flattening a pointer-based tree into a linked list), or traversals of composite and mutually-recursive data types (e.g., copying arbitrary-arity trees).
“Cypress is very fast — it can synthesise many of these programs within a few seconds on a standard laptop,” said A/P Sergey.
This research work is part of an ongoing long-term collaborative effort between A/P Sergey’s research lab and the research group of one of the paper’s co-authors, Assistant Professor Nadia Polikarpova from the University of California, San Diego.
Their joint research agenda focuses on developing practical methodologies for program synthesis of provably correct programs, in languages such as C and Rust.
