# Wei-Ngan Chin

According to our database

Collaborative distances:

^{1}, Wei-Ngan Chin authored at least 120 papers between 1992 and 2018.Collaborative distances:

## Timeline

#### Legend:

Book In proceedings Article PhD thesis Other## Links

#### Homepage:

#### On csauthors.net:

## Bibliography

2018

Automated lemma synthesis in symbolic-heap separation logic.

PACMPL, 2018

A Logical System for Modular Information Flow Verification.

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 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

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.

STTT, 2014

Automated verification of the FreeRTOS scheduler in Hip/Sleek.

STTT, 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

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

Test Case Generation for Adequacy of Floating-point to Fixed-point Conversion.

Electr. Notes Theor. Comput. Sci., 2010

Stack Bound Inference for Abstract Java Bytecode.

Proceedings of the 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, 2010

Dual analysis for proving safety and finding bugs.

Proceedings of the 2010 ACM Symposium on Applied Computing (SAC), 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 Distrib. Comput., 2009

A rigorous methodology for specification and verification of business processes.

Formal Asp. Comput., 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.

ISSE, 2006

Redundant Call Elimination via Tupling.

Fundam. Inform., 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.

Higher-Order and Symbolic Computation, 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 Inf., 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

Extending Sized Type with Collection Analysis.

Proceedings of the Third Asian Workshop on Programming Languages and Systems, 2002

2001

Deriving Pre-conditions for Array Bound Check Elimination.

Proceedings of the Programs as Data Objects, Second Symposium, 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

Calculating Sized Types.

Proceedings of the 2000 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '00), 2000

Calculating a New Data Mining Algorithm for Market Basket Analysis.

Proceedings of the Practical Aspects of Declarative Languages, 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 and Symbolic Computation, 1996

Better Consumers for Program Specializations.

Journal of Functional and Logic Programming, 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.

Computers and Artificial Intelligence, 1995

A Transformation Method for Dynamic-Sized Tabulation.

Acta Inf., 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.

LISP and Functional Programming, 1992

Load Balancing in a Neighbourhood-Based Multiprocessor.

Proceedings of the Parallel Processing: CONPAR 92, 1992