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 (PL), mathematical models of computation, and computer-assisted formal reasoning.

Our results address software reliability issues that arise in everyday job of software developers. we do so by investigating theoretical foundations and building tools for ensuring that certain kinds of costly software errors and vulnerabilities never occur in the real-world code, which many people rely upon in their everyday lives.

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: 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 2: PL Design 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 1, 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.

Theme 3: 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 papers on SuSLik and ROBoSuSLik) 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.

News

Recent

Dec 01

Yutaka Nagashima joins the team as a postdoc. Welcome, Yutaka!

Nov 30

Our paper on Automated Repair of Heap-Manipulating Programs via SuSLik-style Synthesis will appear at VMCAI 2021.

Nov 02

An extended paper on Distributed Protocol Combinators with an expanded toolset and more case studies has been accepted for publication in Journal of Functional Programming. Now we can do Paxos!

Sep 25

Ilya will present the work on CoSplit at PurPL Seminar Series.

Aug 09

Yunjeong Lee and George Pîrlea join the team as a PhD students at NUS School of Computing. Welcome!

Seminars

Recent

Dec 09
KC Sivaramakrishnan(IIT Madras)
Retrofitting Effect Handlers to OCaml
Nov 11
Hila Peleg(UCSD)
Programmer Tools with Program Synthesis
Nov 04
Linghui Luo(Paderborn University)
TaintBench: Automatic Real-World Malware Benchmarking of Android Taint Analyses
Oct 21
Aviral Goel(NEU)
On the Design, Implementation, and Use of Laziness in R
Oct 14
Andreea Costea
ROBoSuSLik: Concise Read-Only Specifications for Better Synthesis of Programs with Pointers

People

Faculty

Ilya Sergey
Ilya Sergey

Postdocs

Andreea Costea
Andreea Costea
Yutaka Nagashima
Yutaka Nagashima

Graduate Students

Kiran Gopinathan
Kiran Gopinathan
Yunjeong Lee
Yunjeong Lee
George Pîrlea
George Pîrlea
Yasunari Watanabe
Yasunari Watanabe

Interns & Research Visitors

Irina Artemeva
Irina Artemeva

Projects

Hippodrome
Static automated concurrency repair at scale.
SuSLik
Synthesis of Heap-Manipulating Programs from Separation Logic specifications.
Ceramist
Verified hash-based approximate membership structures.
Scilla
A functional language for safe smart contracts.
Toychain
A Coq implementation of a minimalistic blockchain-based consensus protocol.
DiSeL
Mechanised Separation Logic for Compositional Verification of Distributed Protocols.

Publications

Recent

Automated Repair of Heap-Manipulating Programs using Deductive Synthesis
Thanh-Toan Nguyen, Quang-Trung Ta, Ilya Sergey and Wei-Ngan Chin

22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2021). Copenhagen, Denmark, January 2021.

Protocol Combinators for Modeling, Testing, and Execution of Distributed Systems
Kristoffer Just Arndal Andersen and Ilya Sergey

Accepted for publication in Journal of Functional Programming in 2021. Cambridge University Press.

Building a Certified Program Synthesizer
Yasunari Watanabe

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

Compiling a Higher-Order Smart Contract Language to LLVM
Vaivaswatha Nagaraj, Jacob Johannsen, Anton Trunov, George Pîrlea, Amrit Kumar and Ilya Sergey

2020 Virtual LLVM Developers' Meeting on the LLVM Compiler Infrastructure, October 2020.

Certifying Certainty and Uncertainty in Approximate Membership Query Structures
Kiran Gopinathan and Ilya Sergey

32nd International Conference on Computer-Aided Verification (CAV 2020). Los Angeles, CA, USA, July 2020.

Concise Read-Only Specifications for Better Synthesis of Programs with Pointers
Andreea Costea, Amy Zhu, Nadia Polikarpova and Ilya Sergey

29th European Symposium on Programming (ESOP 2020). Dublin, Ireland, April 2020.

Safer Smart Contract Programming with Scilla
Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov and Ken Chan Guan Hao

34th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2019). Athens, Greece, October 2019.

Toychain: Formally Verified Blockchain Consensus
George Pîrlea

MEng Thesis. University College London, 2019

Synchronisation Primitives for Smart Contracts
Jake Si Yuan Goh

Capstone Thesis. Yale-NUS College, 2019.

Modelling and Testing Composite Byzantine-Fault Tolerant Consensus Protocols
Daniel Lok

Capstone Thesis. Yale-NUS College, 2019.

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