03 September 2022 — NUS Computing Associate Professor Ilya Sergey and Assistant Professor Trevor Carlson were announced as recipients of the Amazon Research Awards this year.
The Amazon Research Awards is a programme that provides unrestricted funds and Amazon Web Services (AWS) promotional credits to academic researchers investigating research topics across a number of disciplines.
Prof Sergey’s research proposal involves program synthesis, while Prof Carlson’s research proposal involves accelerating the solving of the Boolean Satisfiability (SAT) problem.
According to Amazon, there were a total of 74 awardees from 51 universities in 17 countries this year.
Recipients of the award will have access to more than 300 Amazon public datasets, and will be able to utilise AWS Artificial Intelligence (AI) and Machine Learning (ML) services and tools. The award will also support the work of up to two graduate or postdoctoral students for one year, under the supervision of a faculty member.
Prof Sergey’s research proposal combines the topics of formal verification, distributed systems and program synthesis, research areas which he has been working on over the past few years with his team.
Said Prof Sergey: “I am planning to use the award to fund the research my group does on improving state of the art technology in formal verification of distributed protocols, with the ultimate goal to facilitate industrial adoption of rigorous formal methods for soundness reasoning about real-world distributed systems.”
“The challenge we’re aiming to address is to make rigorous automated verification of newly developed distributed protocols practical and accessible to the developers with little expertise in formal methods,” he explained.
“The existing state of the art approaches require non-trivial expertise to even define protocols and their properties in a way that enables their decidable verification. Our unique vision is to bridge this conceptual gap between the systems code developed by programmers and the formal definitions of protocols that can be verified by using the technology known as ‘program synthesis’,” he said.
The synthesis task in this setting is to automatically produce the model that correctly simulates the behaviour of a real system implementation, yet is phrased in a way that allows for proving of its properties of interest – for example, the crash resilience of a replication protocol – in a fully automated way, he explained.
He added that the team’s approach – using program synthesis techniques for producing formal systems specification with a goal to verify them – is the first of its kind.
“I am delighted and extremely excited to receive the award from Amazon. The researchers from Amazon’s AWS Automated Reasoning division have made remarkable contributions to bring formal methods to software systems engineering in the last couple of years. I look forward to collaborating with AWS, and to apply the techniques developed by my research team on a larger scale,” he added.
