News
Our paper on accelerating SMT-based program verifiers will appear at CAV’25.
A paper on synthesising Separation Logic predicates via Answer Set Programming is accepted at OOPSLA’25.
A paper on programming language synthesis for automated exploit generation is accepted at USENIX Security’25.
Congratulations to Yunjeong Lee and Ziyi Yang on receiving Research Achievement Awards!
A paper on the taxonomy of intents and mechanisms for DSL design in Racket is accepted at SLE’24.
Kiran Gopinathan has successfully defended her PhD thesis “Scaling the Evolution of Verified Software”. Congratulations, Dr. Gopinathan!
Two new papers at upcoming conferences in October 2024: on compositional verification of Byzantine protocols (CCS’24) and on building concurrent data structures via batch-parallelism (OOPSLA’24).
Congratulations to George Pîrlea on receiving a Dean’s Research Excellence Award for 2024!
Our work on higher-order specifications for deductive synthesis in SuSLik will appear at ECOOP’24.
The paper on hyperlogic for verifying sparse tensor programs in Coq will appear at PLDI’24.
Our paper on verifying tree clocks in Coq will appear at CPP’24. Update: We’ve also got a Distinguished Paper Award!
Congratulations to Mayank Keoliya on awarded the 2023 NUS Outstanding Undergraduate Researcher Prize!
Congratulations to Kiran Gopinathan on receiving a Dean’s Research Excellence Award for 2023!
Congratulations to Mayank Keoliya on awarded the 2023 NUS Outstanding Undergraduate Researcher Prize!
The paper on fuzzing distributed systems will appear at CCS’23.
The implementation of RusSOL has won a PLDI’23 Distinguished Artifact Award (single award given out of 67 submitted artifacts).
The paper about Sisyphus received an ACM SIGPLAN Distinguished Paper Award at PLDI’23.
Two papers will appear at PLDI’23: Mostly Automated Proof Repair for Verified Libraries and Leveraging Rust Types for Program Synthesis.
Qiyuan Zhao joins NUS as a PhD Student. Welcome Qiyuan!
Vladimir Gladstein joins VERSE lab as a PhD student. Welcome, Vladimir!
A paper on random testing of Scilla interpreter and compiler with QuickChick will appear at ICFP’22.
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.
Ziyi Yang joins the lab as a PhD student, and Tram Hoang and Bryan Tan join as MComp students. Welcome, Bryan, Tram, and Ziyi!
Kiran will present GopCaml: A Structural Editor for OCaml at OCaml Workshop 2021, co-located with ICFP’21.
The paper on Certifying the Synthesis of Heap-Manipulating Programs will appear at ICFP’21.
Our invited position paper Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities has appeared in the proceedings of CAV’21.
The paper on Cyclic Program Synthesis has been named a recipient of PLDI 2021 Distinguished Paper Award.
Two papers, on smart contract sharding and on cyclic program synthesis, will appear at PLDI’21.
Yasunari Watanabe has defended his MComp thesis on Certified Program Synthesis. Congratulations, Yasu!
Yutaka Nagashima joins the team as a postdoc. Welcome, Yutaka!
Our paper on Automated Repair of Heap-Manipulating Programs via SuSLik-style Synthesis will appear at VMCAI 2021.
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!
Ilya will present the work on CoSplit at PurPL Seminar Series.
Yunjeong Lee and George Pîrlea join the team as a PhD students at NUS School of Computing. Welcome!
The paper by Kiran on mechanised verification of probabilistic properties of Bloom filters and their generalisations has been accepted to CAV 2020.
