| 2025 | SAS | Specifying and Verifying Future Conditions. | Yahui Song, Darius Foo, Wei-Ngan Chin |
| 2025 | TACAS | Inferring Incorrectness Specifications for Object-Oriented Programs. | Wenhua Li, Quang Loc Le, Yahui Song, Wei-Ngan Chin |
| 2024 | FM | Staged Specification Logic for Verifying Higher-Order Imperative Programs. | Darius Foo, Yahui Song, Wei-Ngan Chin |
| 2023 | APLAS | Incorrectness Proofs for Object-Oriented Programs via Subclass Reflection. | Wenhua Li, Quang Loc Le, Yahui Song, Wei-Ngan Chin |
| 2023 | TACAS | Automated Verification for Real-Time Systems - via Implicit Clocks and an Extended Antimirov Algorithm. | Yahui Song, Wei-Ngan Chin |
| 2023 | TASE | Protocol Conformance with Choreographic PlusCal. | Darius Foo, Andreea Costea, Wei-Ngan Chin |
| 2022 | APLAS | Automated Temporal Verification for Algebraic Effects. | Yahui Song, Darius Foo, Wei-Ngan Chin |
| 2021 | VMCAI | Automated Repair of Heap-Manipulating Programs Using Deductive Synthesis. | Thanh-Toan Nguyen, Quang-Trung Ta, Ilya Sergey, Wei-Ngan Chin |
| 2021 | VMCAI | A Synchronous Effects Logic for Temporal Verification of Pure Esterel. | Yahui Song, Wei-Ngan Chin |
| 2020 | ICFEM | Automated Temporal Verification of Integrated Dependent Effects. | Yahui Song, Wei-Ngan Chin |
| 2019 | TACAS | SL-COMP: Competition of Solvers for Separation Logic. | Mihaela Sighireanu, Juan Antonio Navarro Prez, Andrey Rybalchenko, Nikos Gorogiannis, Radu Iosif, Andrew Reynolds, Cristina Serban, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger, Wei-Ngan Chin, Quang Loc Le, Quang-Trung Ta, Ton-Chanh Le, Thanh-Toan Nguyen, Siau-Cheng Khoo, Michal Cyprian, Adam Rogalewicz, Toms Vojnar, Constantin Enea, Ondrej Lengl, Chong Gao, Zhilin Wu |
| 2019 | VMCAI | Automatic Program Repair Using Formal Verification and Expression Templates. | Thanh-Toan Nguyen, Quang-Trung Ta, Wei-Ngan Chin |
| 2018 | APLAS | Automated Modular Verification for Relaxed Communication Protocols. | Andreea Costea, Wei-Ngan Chin, Shengchao Qin, Florin Craciun |
| 2018 | ICECCS | Variant Region Types. | Florin Craciun, Wei-Ngan Chin, Shengchao Qin |
| 2018 | VMCAI | A Logical System for Modular Information Flow Verification. | Adi Prabawa, Mahmudul Faisal Al Ameen, Benedict Lee, Wei-Ngan Chin |
| 2017 | CAV | A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic. | Quang Loc Le, Makoto Tatsuta, Jun Sun, Wei-Ngan Chin |
| 2017 | ICFEM | A Certified Decision Procedure for Tree Shares. | Xuan Bach Le, Thanh-Toan Nguyen, Wei-Ngan Chin, Aquinas Hobor |
| 2017 | TACAS | HipTNT+: A Termination and Non-termination Analyzer by Second-Order Abduction - (Competition Contribution). | Ton Chanh Le, Quang-Trung Ta, Wei-Ngan Chin |
| 2016 | APLAS | Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic. | Makoto Tatsuta, Quang Loc Le, Wei-Ngan Chin |
| 2016 | CAV | Satisfiability Modulo Heap-Based Programs. | Quang Loc Le, Jun Sun, Wei-Ngan Chin |
| 2016 | FM | Automated Mutual Explicit Induction Proof in Separation Logic. | Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, Wei-Ngan Chin |
| 2015 | FM | Certified Reasoning with Infinity. | Asankhaya Sharma, Shengyi Wang, Andreea Costea, Aquinas Hobor, Wei-Ngan Chin |
| 2015 | ICFEM | Specifying Compatible Sharing in Data Structures. | Asankhaya Sharma, Aquinas Hobor, Wei-Ngan Chin |
| 2015 | PEPM | Threads as Resource for Concurrency Verification. | Duy-Khanh Le, Wei-Ngan Chin, Yong Meng Teo |
| 2015 | PLDI | Termination and non-termination specification inference. | Ton Chanh Le, Shengchao Qin, Wei-Ngan Chin |
| 2014 | CAV | Shape Analysis via Second-Order Bi-Abduction. | Quang Loc Le, Cristian Gherghina, Shengchao Qin, Wei-Ngan Chin |
| 2014 | ICFEM | A Resource-Based Logic for Termination and Non-termination Proofs. | Ton Chanh Le, Cristian Gherghina, Aquinas Hobor, Wei-Ngan Chin |
| 2014 | SEFM | Completeness of Separation Logic with Inductive Definitions for Program Verification. | Makoto Tatsuta, Wei-Ngan Chin |
| 2013 | APLAS | Bi-Abduction with Pure Properties for Specification Inference. | Minh-Thai Trinh, Quang Loc Le, Cristina David, Wei-Ngan Chin |
| 2013 | ATVA | An Expressive Framework for Verifying Deadlock Freedom. | Duy-Khanh Le, Wei-Ngan Chin, Yong Meng Teo |
| 2013 | ICFEM | Automated Specification Discovery via User-Defined Predicates. | Guanhua He, Shengchao Qin, Wei-Ngan Chin, Florin Craciun |
| 2013 | ICFEM | Verification of Static and Dynamic Barrier Synchronization Using Bounded Permissions. | Duy-Khanh Le, Wei-Ngan Chin, Yong Meng Teo |
| 2013 | ICFEM | A Proof Slicing Framework for Program Verification. | Ton Chanh Le, Cristian Gherghina, Razvan Voicu, Wei-Ngan Chin |
| 2012 | ICFEM | Variable Permissions for Concurrency Verification. | Duy-Khanh Le, Wei-Ngan Chin, Yong Meng Teo |
| 2012 | TASE | From Verification to Specification Inference. | Wei-Ngan Chin, Cristina David |
| 2011 | CAV | A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification. | Wei-Ngan Chin, Cristian Gherghina, Razvan Voicu, Quang Loc Le, Florin Craciun, Shengchao Qin |
| 2011 | CAV | FixBag: A Fixpoint Calculator for Quantified Bag Constraints. | Tuan-Hung Pham, Minh-Thai Trinh, Anh-Hoang Truong, Wei-Ngan Chin |
| 2011 | FM | Structured Specifications for Better Verification of Heap-Manipulating Programs. | Cristian Gherghina, Cristina David, Shengchao Qin, Wei-Ngan Chin |
| 2011 | FM | Automatically Refining Partial Specifications for Program Verification. | Shengchao Qin, Chenguang Luo, Wei-Ngan Chin, Guanhua He |
| 2011 | OOPSLA | A HIP and SLEEK verification system. | Wei-Ngan Chin, Cristina David, Cristian Gherghina |
| 2011 | OOPSLA | Immutable specifications for more concise and precise verification. | Cristina David, Wei-Ngan Chin |
| 2010 | CADE | Discovering Specifications for Unknown Procedures - Work in Progress. | Florin Craciun, Chenguang Luo, Guanhua He, Shengchao Qin, Wei-Ngan Chin |
| 2010 | ICFEM | Loop Invariant Synthesis in a Combined Domain. | Shengchao Qin, Guanhua He, Chenguang Luo, Wei-Ngan Chin |
| 2010 | ICFEM | Verifying Heap-Manipulating Programs with Unknown Procedure Calls. | Shengchao Qin, Chenguang Luo, Guanhua He, Florin Craciun, Wei-Ngan Chin |
| 2010 | SAC | Dual analysis for proving safety and finding bugs. | Corneliu Popeea, Wei-Ngan Chin |
| 2010 | TASE | Stack Bound Inference for Abstract Java Bytecode. | Shengyi Wang, Zongyan Qiu, Shengchao Qin, Wei-Ngan Chin |
| 2009 | ATVA | Memory Usage Verification Using Hip/Sleek. | Guanhua He, Shengchao Qin, Chenguang Luo, Wei-Ngan Chin |
| 2009 | ESOP | An Interval-Based Inference of Variant Parametric Types. | Florin Craciun, Wei-Ngan Chin, Guanhua He, Shengchao Qin |
| 2009 | PEPM | Translation and optimization for a core calculus with exceptions. | Cristina David, Cristian Gherghina, Wei-Ngan Chin |
| 2009 | SEFM | Completeness of Pointer Program Verification by Separation Logic. | Makoto Tatsuta, Wei-Ngan Chin, Mahmudul Faisal Al Ameen |
| 2008 | APLAS | A Flow-Sensitive Region Inference for CLI. | Alexandru Stefan, Florin Craciun, Wei-Ngan Chin |
| 2008 | CAV | Enhancing Program Verification with Lemmas. | Huu Hai Nguyen, Wei-Ngan Chin |
| 2008 | ICFEM | A Formal Soundness Proof of Region-Based Memory Management for Object-Oriented Paradigm. | Florin Craciun, Shengchao Qin, Wei-Ngan Chin |
| 2008 | PEPM | A practical and precise inference and specializer for array bound checks elimination. | Corneliu Popeea, Dana N. Xu, Wei-Ngan Chin |
| 2008 | POPL | Enhancing modular OO verification with separation logic. | Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin |
| 2008 | SEFM | A Fast Algorithm to Compute Heap Memory Bounds of Java Card Applets. | Tuan-Hung Pham, Anh-Hoang Truong, Ninh-Thuan Truong, Wei-Ngan Chin |
| 2008 | VMCAI | Runtime Checking for Separation Logic. | Huu Hai Nguyen, Viktor Kuncak, Wei-Ngan Chin |
| 2007 | ICECCS | Automated Verification of Shape, Size and Bag Properties. | Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin |
| 2007 | VMCAI | Automated Verification of Shape and Size Properties Via Separation Logic. | Huu Hai Nguyen, Cristina David, Shengchao Qin, Wei-Ngan Chin |
| 2006 | OOPSLA | A flow-based approach for variant parametric types. | Wei-Ngan Chin, Florin Craciun, Siau-Cheng Khoo, Corneliu Popeea |
| 2006 | OOPSLA | Core-java: an expression-oriented java. | Florin Craciun, Hong Yaw Goh, Corneliu Popeea, Wei-Ngan Chin |
| 2006 | SYNASC | Incremental Deterministic Planning. | Stefan Andrei, Wei-Ngan Chin, Martin C. Rinard |
| 2005 | ICSE | Verifying safety policies with size properties and alias controls. | Wei-Ngan Chin, Siau-Cheng Khoo, Shengchao Qin, Corneliu Popeea, Huu Hai Nguyen |
| 2005 | RTAS | Systematic Debugging of Real-Time Systems based on Incremental Satisfiability Counting. | Stefan Andrei, Albert Mo Kim Cheng, Wei-Ngan Chin, Mihai Lupu |
| 2005 | RTCSA | Runtime-Coordinated Scalable Incremental Checksum Testing of Combinational Circuits. | Stefan Andrei, Wei-Ngan Chin, Albert Mo Kim Cheng, Yongxin Zhu |
| 2005 | SAS | Memory Usage Verification for OO Programs. | Wei-Ngan Chin, Huu Hai Nguyen, Shengchao Qin, Martin C. Rinard |
| 2004 | ICTAC | An Automatic Mapping from Statecharts to Verilog. | Viet-Anh Vu Tran, Shengchao Qin, Wei-Ngan Chin |
| 2004 | PEPM | A type system for resource protocol verification and its correctness proof. | Corneliu Popeea, Wei-Ngan Chin |
| 2004 | PLDI | Region inference for an object-oriented language. | Wei-Ngan Chin, Florin Craciun, Shengchao Qin, Martin C. Rinard |
| 2004 | RTAS | Incremental Satisfiability Counting for Real-Time Systems. | Stefan Andrei, Wei-Ngan Chin |
| 2003 | FM | Mapping Statecharts to Verilog for Hardware/Software Co-specification. | Shengchao Qin, Wei-Ngan Chin |
| 2003 | FM | A Semantic Foundation for TCOZ in Unifying Theories of Programming. | Shengchao Qin, Jin Song Dong, Wei-Ngan Chin |
| 2003 | PEPM | Extending sized type with collection analysis. | Wei-Ngan Chin, Siau-Cheng Khoo, Dana N. Xu |
| 2002 | APLAS | Extending Sized Type with Collection Analysis. | Wei-Ngan Chin, Siau-Cheng Khoo, Dana N. Xu |
| 2002 | APLAS | A Type-Based Approach to Parallelization (preliminary report). | Dana N. Xu, Siau-Cheng Khoo, Wei-Ngan Chin, Zhenjiang Hu |
| 2002 | GPCE | Towards a Modular Program Derivation via Fusion and Tupling. | Wei-Ngan Chin, Zhenjiang Hu |
| 2002 | ICTAI | A Lazy Divide and Conquer Approach to Constraint Solving. | Saswat Anand, Wei-Ngan Chin, Siau-Cheng Khoo |
| 2001 | APLAS | Higher-Order Polymorphic Sized Types for Safety Checks. | Wei-Ngan Chin, Siau-Cheng Khoo, Dana N. Xu |
| 2001 | ICFP | Charting Patterns on Price History. | Saswat Anand, Wei-Ngan Chin, Siau-Cheng Khoo |
| 2000 | APLAS | Deriving Pre-Conditions for Array Bound Check Elimination. | Wei-Ngan Chin, Siau-Cheng Khoo, Dana N. Xu |
| 2000 | PADL | Calculating a New Data Mining Algorithm for Market Basket Analysis. | Zhenjiang Hu, Wei-Ngan Chin, Masato Takeichi |
| 2000 | PEPM | Calculating Sized Types. | Wei-Ngan Chin, Siau-Cheng Khoo |
| 2000 | SAS | Deriving Parallel Codes via Invariants. | Wei-Ngan Chin, Siau-Cheng Khoo, Zhenjiang Hu, Masato Takeichi |
| 1999 | PEPM | Effective Optimization of Multiple Traversals in Lazy Languages. | Wei-Ngan Chin, Aik-Hui Goh, Siau-Cheng Khoo |
| 1998 | ESOP | Synchronisation Analysis to Stop Tulping. | Wei-Ngan Chin, Siau-Cheng Khoo, Tat-Wee Lee |
| 1998 | POPL | Parallelization in Calculational Forms. | Zhenjiang Hu, Masato Takeichi, Wei-Ngan Chin |
| 1997 | ICFP | A Bounds Inference Method for Vector-Based Memoisation. | Wei-Ngan Chin, Masami Hagiya |
| 1996 | EuroPar | Parallelizing Conditional Recurrences. | Wei-Ngan Chin, John Darlington, Yike Guo |
| 1993 | PEPM | Towards an Automated Tupling Strategy. | Wei-Ngan Chin |
| 1993 | SAS | Tupling Functions with Multiple Recursion Parameters. | Wei-Ngan Chin, Siau-Cheng Khoo |
| 1992 | PEPM | Fully Lazy Higher-Order Removal. | Wei-Ngan Chin |