Wei-Ngan Chin

Orcid: 0000-0002-9660-5682

Affiliations:
  • National University of Singapore (NUS)


According to our database1, Wei-Ngan Chin authored at least 138 papers between 1990 and 2023.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
Staged Specifications for Automated Verification of Higher-Order Imperative Programs.
CoRR, 2023

Tracing OCaml Programs.
CoRR, 2023

Protocol Conformance with Choreographic PlusCal.
Proceedings of the Theoretical Aspects of Software Engineering, 2023

Automated Verification for Real-Time Systems - via Implicit Clocks and an Extended Antimirov Algorithm.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Incorrectness Proofs for Object-Oriented Programs via Subclass Reflection.
Proceedings of the Programming Languages and Systems - 21st Asian Symposium, 2023

2022
Automated Verification for Real-Time Systems using Implicit Clocks and an Extended Antimirov Algorithm.
Proceedings of the Companion Proceedings of the 2022 ACM SIGPLAN International Conference on Systems, 2022

Automated Temporal Verification for Algebraic Effects.
Proceedings of the Programming Languages and Systems - 20th Asian Symposium, 2022

2021
Automated Modular Verification for Race-Free Channels with Implicit and Explicit Synchronization.
CoRR, 2021

A Synchronous Effects Logic for Temporal Verification of Pure Esterel.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2021

Automated Repair of Heap-Manipulating Programs Using Deductive Synthesis.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2021

2020
Automated Temporal Verification of Integrated Dependent Effects.
Proceedings of the Formal Methods and Software Engineering, 2020

2019
Completeness and expressiveness of pointer program verification by separation logic.
Inf. Comput., 2019

Automated mutual induction proof in separation logic.
Formal Aspects Comput., 2019

Automated Verification of CountDownLatch.
CoRR, 2019

Automatic Program Repair Using Formal Verification and Expression Templates.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2019


2018
Automated lemma synthesis in symbolic-heap separation logic.
Proc. ACM Program. Lang., 2018

A Logical System for Modular Information Flow Verification.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2018

Verification of C Buffer Overflows in C Programs.
Proceedings of the 2018 17th RoEduNet Conference: Networking in Education and Research (RoEduNet), 2018

Variant Region Types.
Proceedings of the 23rd International Conference on Engineering of Complex Computer Systems, 2018

Automated Modular Verification for Relaxed Communication Protocols.
Proceedings of the Programming Languages and Systems - 16th Asian Symposium, 2018

2017
Automated specification inference in a combined domain via user-defined predicates.
Sci. Comput. Program., 2017

UStore: A Distributed Storage With Rich Semantics.
CoRR, 2017

HipTNT+: A Termination and Non-termination Analyzer by Second-Order Abduction - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

A Certified Decision Procedure for Tree Shares.
Proceedings of the Formal Methods and Software Engineering, 2017

A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2016
Automated Mutual Explicit Induction Proof in Separation Logic.
Proceedings of the FM 2016: Formal Methods, 2016

Satisfiability Modulo Heap-Based Programs.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic.
Proceedings of the Programming Languages and Systems - 14th Asian Symposium, 2016

2015
Selected and extended papers from Partial Evaluation and Program Manipulation 2014.
Sci. Comput. Program., 2015

Termination and non-termination specification inference.
Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

Threads as Resource for Concurrency Verification.
Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, 2015

Specifying Compatible Sharing in Data Structures.
Proceedings of the Formal Methods and Software Engineering, 2015

Certified Reasoning with Infinity.
Proceedings of the FM 2015: Formal Methods, 2015

2014
Expressive program verification via structured specifications.
Int. J. Softw. Tools Technol. Transf., 2014

Automated verification of the FreeRTOS scheduler in Hip/Sleek.
Int. J. Softw. Tools Technol. Transf., 2014

Automatically refining partial specifications for heap-manipulating programs.
Sci. Comput. Program., 2014

Completeness of Separation Logic with Inductive Definitions for Program Verification.
Proceedings of the Software Engineering and Formal Methods - 12th International Conference, 2014

A Resource-Based Logic for Termination and Non-termination Proofs.
Proceedings of the Formal Methods and Software Engineering, 2014

Shape Analysis via Second-Order Bi-Abduction.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013
Dual analysis for proving safety and finding bugs.
Sci. Comput. Program., 2013

Loop invariant synthesis in a combined abstract domain.
J. Symb. Comput., 2013

Towards Complete Specifications with an Error Calculus.
Proceedings of the NASA Formal Methods, 2013

A Proof Slicing Framework for Program Verification.
Proceedings of the Formal Methods and Software Engineering, 2013

Verification of Static and Dynamic Barrier Synchronization Using Bounded Permissions.
Proceedings of the Formal Methods and Software Engineering, 2013

Automated Specification Discovery via User-Defined Predicates.
Proceedings of the Formal Methods and Software Engineering, 2013

Specification, Verification and Inference (Invited Talk).
Proceedings of the 1st French Singaporean Workshop on Formal Methods and Applications, 2013

Invariants Synthesis over a Combined Domain for Automated Program Verification.
Proceedings of the Theories of Programming and Formal Methods, 2013

An Expressive Framework for Verifying Deadlock Freedom.
Proceedings of the Automated Technology for Verification and Analysis, 2013

Bi-Abduction with Pure Properties for Specification Inference.
Proceedings of the Programming Languages and Systems - 11th Asian Symposium, 2013

2012
Automated verification of shape, size and bag properties via user-defined predicates in separation logic.
Sci. Comput. Program., 2012

From Verification to Specification Inference.
Proceedings of the Sixth International Symposium on Theoretical Aspects of Software Engineering, 2012

Structured specification for program verification.
Proceedings of the Fourth International Conference on Knowledge and Systems Engineering, 2012

Variable Permissions for Concurrency Verification.
Proceedings of the Formal Methods and Software Engineering, 2012

2011
Immutable specifications for more concise and precise verification.
Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2011

A HIP and SLEEK verification system.
Proceedings of the Companion to the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2011

Automatically Refining Partial Specifications for Program Verification.
Proceedings of the FM 2011: Formal Methods, 2011

Structured Specifications for Better Verification of Heap-Manipulating Programs.
Proceedings of the FM 2011: Formal Methods, 2011

FixBag: A Fixpoint Calculator for Quantified Bag Constraints.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

2010
Verifying pointer safety for programs with unknown calls.
J. Symb. Comput., 2010

Stack Bound Inference for Abstract Java Bytecode.
Proceedings of the 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, 2010

Verifying Heap-Manipulating Programs with Unknown Procedure Calls.
Proceedings of the Formal Methods and Software Engineering, 2010

Loop Invariant Synthesis in a Combined Domain.
Proceedings of the Formal Methods and Software Engineering, 2010

Discovering Specifications for Unknown Procedures - Work in Progress.
Proceedings of the Second International Workshop on Invariant Generation, 2010

2009
Optimizing the parallel computation of linear recurrences using compact matrix representations.
J. Parallel Distributed Comput., 2009

A rigorous methodology for specification and verification of business processes.
Formal Aspects Comput., 2009

Test Case Generation for Adequacy of Floating-point to Fixed-point Conversion.
Proceedings of the 3rd International Workshop on Harnessing Theories for Tool Support in Software, 2009

Completeness of Pointer Program Verification by Separation Logic.
Proceedings of the Seventh IEEE International Conference on Software Engineering and Formal Methods, 2009

Translation and optimization for a core calculus with exceptions.
Proceedings of the 2009 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, 2009

An Interval-Based Inference of Variant Parametric Types.
Proceedings of the Programming Languages and Systems, 2009

Memory Usage Verification Using Hip/Sleek.
Proceedings of the Automated Technology for Verification and Analysis, 2009

2008
Runtime Checking for Separation Logic.
Proceedings of the Verification, 2008

A Fast Algorithm to Compute Heap Memory Bounds of Java Card Applets.
Proceedings of the Sixth IEEE International Conference on Software Engineering and Formal Methods, 2008

Enhancing modular OO verification with separation logic.
Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008

A practical and precise inference and specializer for array bound checks elimination.
Proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, 2008

Analysing memory resource bounds for low-level programs.
Proceedings of the 7th International Symposium on Memory Management, 2008

A Formal Soundness Proof of Region-Based Memory Management for Object-Oriented Paradigm.
Proceedings of the Formal Methods and Software Engineering, 2008

Enhancing Program Verification with Lemmas.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008

A Flow-Sensitive Region Inference for CLI.
Proceedings of the Programming Languages and Systems, 6th Asian Symposium, 2008

2007
Automated Verification of Shape and Size Properties Via Separation Logic.
Proceedings of the Verification, 2007

Automated Verification of Shape, Size and Bag Properties.
Proceedings of the 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), 2007

Multiple Pre/Post Specifications for Heap-Manipulating Methods.
Proceedings of the Tenth IEEE International Symposium on High Assurance Systems Engineering (HASE 2007), 2007

2006
Automatic Debugging of Real-Time Systems Based on Incremental Satisfiability Counting.
IEEE Trans. Computers, 2006

From Statecharts to Verilog: a formal approach to hardware/software co-specification.
Innov. Syst. Softw. Eng., 2006

Redundant Call Elimination via Tupling.
Fundam. Informaticae, 2006

Incremental Deterministic Planning.
Proceedings of the 8th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2006), 2006

Core-java: an expression-oriented java.
Proceedings of the Companion to the 21th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2006

A flow-based approach for variant parametric types.
Proceedings of the 21th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2006

Inferring Disjunctive Postconditions.
Proceedings of the Advances in Computer Science, 2006

2005
Memory Usage Verification for OO Programs.
Proceedings of the Static Analysis, 12th International Symposium, 2005

Runtime-Coordinated Scalable Incremental Checksum Testing of Combinational Circuits.
Proceedings of the 11th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2005), 2005

Systematic Debugging of Real-Time Systems based on Incremental Satisfiability Counting.
Proceedings of the 11th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2005), 2005

Verifying safety policies with size properties and alias controls.
Proceedings of the 27th International Conference on Software Engineering (ICSE 2005), 2005

2004
Editorial: Theme Issue on Partial Evaluation and Semantics-Based Program Manipulation.
High. Order Symb. Comput., 2004

Solving a class of higher-order equations over a group structure.
J. Symb. Comput., 2004

Co-determinism and unambiguity of automata accepting finite or infinite words.
Sci. Ann. Cuza Univ., 2004

Self-embedded context-free grammars with regular counterparts.
Acta Informatica, 2004

Incremental Satisfiability Counting for Real-Time Systems.
Proceedings of the 10th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2004), 2004

Region inference for an object-oriented language.
Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation 2004, 2004

A type system for resource protocol verification and its correctness proof.
Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2004

An Automatic Mapping from Statecharts to Verilog.
Proceedings of the Theoretical Aspects of Computing, 2004

2003
A new algorithm for regularizing one-letter context-free grammars.
Theor. Comput. Sci., 2003

Extending sized type with collection analysis.
Proceedings of the 2003 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2003

A Semantic Foundation for TCOZ in Unifying Theories of Programming.
Proceedings of the FME 2003: Formal Methods, 2003

Mapping Statecharts to Verilog for Hardware/Software Co-specification.
Proceedings of the FME 2003: Formal Methods, 2003

2002
An Efficient Distributed Deadlock Avoidance Algorithm for the AND Model.
IEEE Trans. Software Eng., 2002

A Tutorial on a Monadic Approach for Expressions Evaluation.
Sci. Ann. Cuza Univ., 2002

A Lazy Divide and Conquer Approach to Constraint Solving.
Proceedings of the 14th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2002), 2002

Towards a Modular Program Derivation via Fusion and Tupling.
Proceedings of the Generative Programming and Component Engineering, 2002

A Type-Based Approach to Parallelization (preliminary report).
Proceedings of the Third Asian Workshop on Programming Languages and Systems, 2002

2001
Calculating Sized Types.
High. Order Symb. Comput., 2001

Calculating a New Data Mining Algorithm for Market Basket Analysis.
J. Funct. Log. Program., 2001

Charting Patterns on Price History.
Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP '01), 2001

Higher-Order Polymorphic Sized Types for Safety Checks.
Proceedings of the Second Asian Workshop on Programming Languages and Systems, 2001

2000
Deriving Parallel Codes via Invariants.
Proceedings of the Static Analysis, 7th International Symposium, 2000

Deriving Pre-Conditions for Array Bound Check Elimination.
Proceedings of the First Asian Workshop on Programming Languages and Systems, 2000

1999
Effective Optimization of Multiple Traversals in Lazy Languages.
Proceedings of the 1999 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, 1999

1998
Parallelization in Calculational Forms.
Proceedings of the POPL '98, 1998

Parallelization via Context Preservation.
Proceedings of the 1998 International Conference on Computer Languages, 1998

Synchronisation Analysis to Stop Tulping.
Proceedings of the Programming Languages and Systems - ESOP'98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28, 1998

1997
A Bounds Inference Method for Vector-Based Memoisation.
Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP '97), 1997

Deriving efficient parallel programs for complex recurrences.
Proceedings of the 2nd International Workshop on Parallel Symbolic Computation, 1997

1996
A Higher-Order Removal Method.
LISP Symb. Comput., 1996

Better Consumers for Program Specializations.
J. Funct. Log. Program., 1996

Parallelizing Conditional Recurrences.
Proceedings of the Euro-Par '96 Parallel Processing, 1996

Synchronization Analyses for Multiple Recursion Parameters (Extended Abstract).
Proceedings of the Partial Evaluation, International Seminar, 1996

Variable Timestamp-Based Distributed Deadlock Detection and Resolution.
Proceedings of the Concurrency and Parallelism, 1996

1995
Load Balancing and Scheduling in a Neighbourhood-Based Multiprocessor.
Comput. Artif. Intell., 1995

A Transformation Method for Dynamic-Sized Tabulation.
Acta Informatica, 1995

Better Consumers for Deforestation (Extended Abstract)
Proceedings of the Programming Languages: Implementations, 1995

1994
Safe Fusion of Functional Expressions II: Further Improvements.
J. Funct. Program., 1994

1993
Tupling Functions with Multiple Recursion Parameters.
Proceedings of the Static Analysis, Third International Workshop, 1993

Towards an Automated Tupling Strategy.
Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 1993

1992
Fully Lazy Higher-Order Removal.
Proceedings of the PEPM'92, 1992

Safe Fusion of Functional Expressions.
Proceedings of the Conference on Lisp and Functional Programming, 1992

Load Balancing in a Neighbourhood-Based Multiprocessor.
Proceedings of the Parallel Processing: CONPAR 92, 1992

1990
Automatic methods for program transformation.
PhD thesis, 1990


  Loading...