VERSE
Verified Systems Engineering @ NUS
Building trustworthy safety-critical systems and advancing the state of the art in formal verification

About Us

Group photo

We do research in the design and implementation of programming languages, program synthesis and repair, and computer-assisted formal reasoning about complex systems, at School of Computing at National University of Singapore, as a part of PLSE@NUS lab.

Announcements

We are actively looking for motivated PhD students! Get in touch with Ilya Sergey if you want to chat about research opportunities, and apply here. The next application deadline is 15 December.

Two postdoc positions are available in a joint project with Abhik Roychoudhury on automated program repair via static analysis and verification. Check out the project page for the details and get in touch!

Research Themes

Our current investigations follow the themes outlined below.

For more details on our research, check out our blog posts, projects, and recent papers.

Theme 1: Program Synthesis and Repair

Program synthesis is an emerging research and technology paradigm for automatically deriving programs from user-provided declarative specifications, thereby significantly reducing the implementation effort required for producing correct-by-construction and efficient code.

Our recent work explored applications of state-of-the-art techniques for analysis, verification, and deductive proofs for fast and expressive program synthesis (check out the paper on SuSLik, and on the grand challenges in deductive synthesis of program with pointers) and for program repair. Our long-term agenda involves synthesis of correct concurrent and distributed programs by adopting our work on static analysis and logical foundations for reasoning about concurrent and distributed systems.

Theme 2: Trustworthy Distributed Systems

It is hard to overstate the significance and ubiquity of distributed services in many aspects of modern life, such as health care, online commerce, transportation, entertainment and cloud-based applications. Given the importance of distributed software and its complexity, it is vital in industry to have a rigorous verification methodology for establishing its correctness properties, ensuring that, once a distributed system is up and running, it will never go wrong and will eventually complete its goals.

Our recent work has established logical foundations for compositional verification of complex distributed protocols using a proof assistant. We have also produced the first mechanically verified proof of safety of Nakamoto consensus. Our ongoing work builds libraries and techniques for mechanised reasoning about probabilistic properties of distributed protocols and data structures employed by them. In particular, we have produced the first mechanised proof of the false-positive ratio for Bloom filters (see this blog post for more details).

Theme 3: Languages for Distributed Programming

In this line of research we apply core PL techniques, such as semantics, type systems, and abstract interpretation, for building safe and secure decentralised applications.

For instance, in our recent work, inspired by the verification ideas from Theme 2, we have developed a library for compositional construction of distributed protocols, allowing their modular testing and model-checking. By reflecting on the analogy between design principles of secure smart contracts (a particularly prominent class of decentralised applications) and concurrent software (also see the related ACSAC'18 and ISSTA'19 papers), in collaboration with industry partners we have developed Scilla, a functional smart contract language with strong safety guarantees. We have also developed a set of efficient compilation techniques for Scilla as well as a Coq-powered verification methodology for it.

Our ongoing research explores opportunities for (a) developing low-overhead abstractions for automated reasoning about distributed applications and (b) enhancing parallelism offered by modern distributed protocols via programming language techniques.

People

Faculty

Ilya Sergey
Ilya Sergey

Postdocs

Andreea Costea
Andreea Costea

Graduate Students

Vladimir Gladstein
Vladimir Gladstein
Kiran Gopinathan
Kiran Gopinathan
Yunjeong Lee
Yunjeong Lee
Ruijie Meng
Ruijie Meng
George Pîrlea
George Pîrlea
Ziyi Yang
Ziyi Yang
Qiyuan Zhao
Qiyuan Zhao

Undergraduate Researchers

Karolina Grzeszkiewicz
Karolina Grzeszkiewicz
Mayank Keoliya
Mayank Keoliya
Koon Wen Lee
Koon Wen Lee
Theodore Leebrant
Theodore Leebrant
Sewen Thy
Sewen Thy

News

Recent

Jan 10

Qiyuan Zhao joins NUS as a PhD Student. Welcome Qiyuan!

Jul 18

Vladimir Gladstein joins VERSE lab as a PhD student. Welcome, Vladimir!

Jul 01

A paper on random testing of Scilla interpreter and compiler with QuickChick will appear at ICFP’22.

Jun 20

Our paper on Hippodrome, a new tool for automated repair of concurrent data races, built on top of Infer Static Analyser, will appear at ACM Transactions on Software Engineering and Methodology.

Sep 01

Ziyi Yang joins the lab as a PhD student, and Tram Hoang and Bryan Tan join as MComp students. Welcome, Bryan, Tram, and Ziyi!

Projects

ego
An OCaml library that provides generic equality saturation using EGraphs.
SuSLik
Synthesis of Heap-Manipulating Programs from Separation Logic specifications.
Scilla
A functional language for safe smart contracts.
Ceramist
Verified hash-based approximate membership structures.
Toychain
A Coq implementation of a minimalistic blockchain-based consensus protocol.
DiSeL
Mechanised Separation Logic for Compositional Verification of Distributed Protocols.

Publications

Recent

Random Testing of a Higher-Order Blockchain Language (Experience Report)
Tram Hoang, Anton Trunov, Leonidas Lampropoulos and Ilya Sergey

27th ACM SIGPLAN International Conference on Functional Programming (ICFP 2022). Ljubljana, Slovenia, September 2022.

HIPPODROME: Data Race Repair using Static Analysis Summaries
Andreea Costea, Abhishek Tiwari, Sigmund Chianasta, Kishore R, Abhik Roychoudhury and Ilya Sergey

ACM Transactions on Software Engineering and Methodology. 2022.

From C towards Idiomatic & Safer Rust through Constraints-Guided Refactoring
Bryan Tan Yao Hong

MComp Thesis. NUS School of Computing, 2022.

Synthesizing Musical Harmony using Equality Graphs
Juwon Lee

Capstone Thesis. Yale-NUS College, 2022.

Verifying Distributed Protocols: From Executable to Decidable
Mark Yuen

Capstone Thesis. Yale-NUS College, 2022.

A Lazy Desugaring System for Evaluating Programs with Sugars
Ziyi Yang, Yushuo Xiao, Zhichao Guan and Zhenjiang Hu

16th International Symposium on Functional and Logic Programming (FLOPS 2022). Taking place virtually, May 2022.

The Next 700 Smart Contract Languages
Ilya Sergey

Principles of Blockchain Systems 2021. Pages 69–94. Morgan & Claypool. Author’s version.

Certifying the Synthesis of Heap-Manipulating Programs
Yasunari Watanabe, Kiran Gopinathan, George Pîrlea, Nadia Polikarpova and Ilya Sergey

26th ACM SIGPLAN International Conference on Functional Programming (ICFP 2021). Taking place virtually, August 2021.

GopCaml: A Structural Editor for OCaml
Kiran Gopinathan

2021 OCaml Users and Developers Workshop (OCaml 2021). Taking place virtually, August 2021.

Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities (Invited Paper)
Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben Rowe and Ilya Sergey

33rd International Conference on Computer-Aided Verification (CAV 2021). Taking place virtually, July 2021.

VERSE
Verified Systems Engineering
Yale-NUS College
NUS School of Computing