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 computer-assisted formal reasoning about complex systems, at the School of Computing of National University of Singapore, as a part of PLSE@NUS lab.

Announcements

Postdoc positions are available in a project on automated program repair via static analysis and verification. Check out the project page for the details and get in touch!

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.

Research internships: In case if you are interested in an internship with us, please get in touch with your CV and a paragraph of text describing your specific interests in the research themes we pursue at the moment. Strong background in PL/logic/verification or systems-building is a must. We welcome candidates who will commit six months or longer to focused research on-site.

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: Certified Program Synthesis

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 the marriage of state-of-the-art techniques for deductive proofs in Coq proof assistant and program synthesis that resulted in a series of tools that produce correct-by construction implementations for complex tasks in mainstream languages.

Our long-term agenda targets synthesis of provably correct high-performance, safety-critical programs with the focus on low-effort proof automation and evolution.

Theme 2: Safe and Efficient Concurrency

Despite being one of the oldest topics in Computer Science, concurrent programming still poses multiple challenges from both theoretical and practical standpoint: concurrent libraries that utilise available opportunities for parallelism are difficult to implement, optimise, and verify, and bugs in concurrent programs are extremely tricky to identify and fix. To address these challenges, we have developed foundations for machine-assisted verification of concurrent programs. We have also contributed tools for fast compositional bug-funding in concurrent code with theoretical completeness guarantees, and developed a methodology for efficient repair of concurrent bugs. Finally, we used the ideas from static program analysis and type systems to improve system-wide parallelism in modern blockchain protocols.

Our vision in this line of work is to democratise the process implementation of concurrent libraries and applications, developing robust and accessible methods for building correct and performant concurrent programs.

Theme 3: Towards Trustworthy Evolving Software Systems

Given the importance of modern software systems (e.g., distributed systems, concurrency and high-performance computing libraries, etc) and their complexity, it is vital in industry to have a rigorous verification methodology for establishing their correctness properties as well as for making sure that the once completed proofs don’t go “bit rot”. In this line of work, our recent work has introduced 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, its probabilistic properties and verified libraries of relevant probabilistic data structures. We also explored techniques for lightweight verification of distributed systems, such as greybox fuzzing. Finally, we have developed the first approach for (mostly) automated evolution of proofs for verified libraries.

Our long-term goal is to build tools that bridge the gap between the systems implementations and their abstract models that can be verified in an interactive or automated fashion, producing robust and easy-to-maintain proofs.

People

Faculty

Ilya Sergey
Ilya Sergey

Graduate Students

Vladimir Gladshtein
Vladimir Gladshtein
Kiran Gopinathan
Kiran Gopinathan
Yunjeong Lee
Yunjeong Lee
Yuxi Ling
Yuxi Ling
George Pîrlea
George Pîrlea
Ziyi Yang
Ziyi Yang
Qiyuan Zhao
Qiyuan Zhao

Undergraduate Researchers

Vikram Goyal
Vikram Goyal
Gokul Rajiv
Gokul Rajiv

Recent Collaborators

Willow Ahrens
Willow Ahrens
Saman Amarasinghe
Saman Amarasinghe
Zhendong Ang
Zhendong Ang
Andreea Costea
Andreea Costea
Jonáš Fiala
Jonáš Fiala
Matthew Flatt
Matthew Flatt
Seth Gilbert
Seth Gilbert
Shachar Itzhaky
Shachar Itzhaky
Leonidas Lampropoulos
Leonidas Lampropoulos
Umang Mathur
Umang Mathur
Peter Müller
Peter Müller
Nadia Polikarpova
Nadia Polikarpova
Alex Potanin
Alex Potanin
Abhik Roychoudhury
Abhik Roychoudhury

News

Recent

Dec 13

Our paper on verifying tree clocks in Coq will appear at CPP’24. Update: We’ve also got a Distinguished Paper Award!

Aug 28

Congratulations to Mayank Keoliya on awarded the 2023 NUS Outstanding Undergraduate Researcher Prize!

Aug 24

Congratulations to Kiran Gopinathan on receiving a Dean’s Research Excellence Award!

Aug 28

Congratulations to Mayank Keoliya on awarded the 2023 NUS Outstanding Undergraduate Researcher Prize!

Aug 11

The paper on fuzzing distributed systems will appear at CCS’23.

Projects

Sisyphus

Mostly automated proof repair for verified OCaml functions

RusSOL

Synthesis of Rust programs from types and lightweight specifications

SuSLik

Synthesis of heap-manipulating programs from specifications in Separation Logic

Scilla

A functional language for safe smart contracts

ego

An OCaml library that provides generic equality saturation using EGraphs

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

Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic

Qiyuan Zhao and George Pîrlea and Zhendong Ang and Umang Mathur and Ilya Sergey

13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024). London, UK, January 2024. Distinguished Paper Award.

PDF Code Artefact

Greybox Fuzzing of Distributed Systems

Ruijie Meng and George Pîrlea and Abhik Roychoudhury and Ilya Sergey

30th ACM Conference on Computer and Communications Security (CCS 2023). Copenhagen, Denmark, December 2023.

PDF Code

Adventure of a Lifetime: Extract Method Refactoring for Rust

Sewen Thy and Andreea Costea and Kiran Gopinathan and Ilya Sergey

38th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2023). Lisbon, Portugal, October 2023.

Mostly Automated Proof Repair for Verified Libraries

Kiran Gopinathan and Mayank Keoliya and Ilya Sergey

2023 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023). Orlando, FL, USA, June 2023. ACM SIGPLAN Distinguished Paper Award

Leveraging Rust Types for Program Synthesis

Jonas Fiala and Shachar Itzhaky and Peter Müller and Nadia Polikarpova and Ilya Sergey

2023 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023). Orlando, FL, USA, June 2023. Distinguished Artifact Award

Borrowing without Sorrowing: Implementing Extract Method Refactoring for Rust

Sewen Thy

Capstone Thesis. Yale-NUS College, 2023. Recipient of the Outstanding Yale-NUS Capstone Prize for 2023.

Formally Verifying Accountable Byzantine Consensus

Karolina Grzeszkiewicz

Capstone Thesis. Yale-NUS College, 2023.

Concurrent Structures and Effect Handlers: A Batch Made in Heaven

Koon Wen Lee

Capstone Thesis. Yale-NUS College, 2023.

HIPPODROME: Data Race Repair using Static Analysis Summaries

Andreea Costea and Abhishek Tiwari and Sigmund Chianasta and Kishore R and Abhik Roychoudhury and Ilya Sergey

ACM Transactions on Software Engineering and Methodology. 2023.

Random Testing of a Higher-Order Blockchain Language (Experience Report)

Tram Hoang and Anton Trunov and Leonidas Lampropoulos and Ilya Sergey

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

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