Multiple Pre/Post Specifications for Heap-Manipulating Methods (2008)
Abstract Automated verification plays an important role forhigh assurance software. This approach typically uses a pair of pre/post conditions as a formal (but possiblypartial) specification of each...
A Type-Safe Embedding of Constraint Handling (2008)
Rules Into Haskell, Wei-ngan Chin, Martin Sulzmann, Meng Wang
Multiple Pre/Post Specifications for Heap-Manipulating Methods (2008)
Automated verification plays an important role for high assurance software. This typically uses a pair of pre/post conditions as a formal (but possibly partial) specification of each method before it...
A Region Memory Subsystem for SSCLI (2008)
Ru Stefan, Florin Craciun, Wei-ngan Chin
Abstract. Region-based memory management can offer improved time performance, relatively good memory locality and reuse, and also provide better adherence to real-time constraints during execution,...
(Preliminary Report) Abstract (2008)
Wei-ngan Chin, Siau-cheng Khoo, Peter Thiemann
Tupling is a transformation tactic to obtain new functions, without redundant calls and/or multiple traversals of common inputs. In [Chi93], we presented an automatic method for tupling functions...
ABSTRACT Region Inference for an Object-Oriented Language (2008)
Wei-ngan Chin, Shengchao Qin, Martin Rinard
Region-based memory management offers several important potential advantages over garbage collection, including real-time performance, better data locality, and more efficient use of limited memory....
Huu Hai Nguyen, Wei-ngan Chin, Shengchao Qin, Martin Rinard
Abstract — We present a type-based approach to statically derive symbolic closed-form formulae that characterize the bounds of heap memory usages of programs written in object-oriented languages....
Solving a Class of Higher-Order Equations over a Group Structure (2008)
In recent years, symbolic and constraint-solving techniques have been making major advances and are continually being deployed in new business and engineering applications. A major push behind this...
Runtime Checking for Separation Logic (2008)
Huu Hai Nguyen, Viktor Kuncak, Wei-ngan Chin
Abstract. Separation logic is a popular approach for specifying properties of recursive mutable data structures. Several existing systems verify a subclass of separation logic specifications using...
ABSTRACT Region Inference for an Object-Oriented Language (2008)
Wei-ngan Chin, Florin Craciun, Shengchao Qin, Martin Rinard
Region-based memory management offers several important potential advantages over garbage collection, including real-time performance, better data locality, and more efficient use of limited memory....
Region Type Checking for Core-Java (2008)
Wei-ngan Chin, Shengchao Qin, Martin Rinard
Abstract — Region-based memory management offers several important advantages over garbage-collected heap, including real-time performance, better data locality and efficient use of limited memory....
Runtime Checking for Separation Logic (2008)
Huu Hai Nguyen, Viktor Kuncak, Wei-ngan Chin
Abstract. Separation logic is a popular approach for specifying properties of recursive mutable data structures. Several existing systems verify a subclass of separation logic specifications using...
Incremental Verification of Timing Constraints for Real-Time Systems (2008)
Abstract — Testing constraints for real-time systems are usually verified through the satisfiability of propositional formulae. In this paper, we propose an alternative where the verification of...
A New Constructive Method for the One-Letter Context-Free Grammars (2008)
Abstract — Constructive methods for obtaining the regular grammar counterparts for some sub-classes of the context free grammars (cfg) have been investigated by many researchers. An important class...
Abstract The dynamic-sized tabulation method can be used to elim- inate redundant calls for certain classes of recursive pro- grams. An innovative aspect of the method is the use of lambda...
A Type System for Parallelization (2008)
Dana N. Xu, Siau-cheng Khoo, Wei-ngan Chin, Zhenjiang Hu
Parallel programming is becoming an important cornerstone of general computing. In addition, type systems have significant impact on program analysis. In this paper, we demonstrate an automated...
Enhancing modular OO verification with separation logic (2008)
Wei-ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin
chinwn,davidcri,nguyenh2© Conventional specifications for object-oriented (OO) programs must adhere to behavioral subtyping in support of class inheritance and method overriding. However, this...
A Case Study on a Modular Transformation Strategy (2007)
Zhenjiang Hu, Wei-ngan Chin, Masato Takeichi
Transformational programming is a well-known methodology to derive both correct and efficient programs. But it often requires deep insights to make major jumps during derivation, and so it remains...
A type-based approach to parallelization (2007)
Dana N. Xu, Siau-cheng Khoo, Wei-ngan Chin, Zhenjiang Hu
Parallel programs can be synthesized from sequential functional programs via a technique known as context preservation [6]. This technique has significantly broadened the set of sequential programs...
Towards a Modular Program Derivation via Fusion and Tupling (2007)
We show how programming pearls can be systematically derived via fusion, followed by tupling transformations. By focusing on the elimination of intermediate data structures (fusion) followed by the...
Charting Patterns on Price History (2007)
Saswat An, Wei-ngan Chin, Siau-cheng Khoo
It is an established notion among financial analysts that price moves in patterns and these patterns can be used to forecast future price. As the definitions of these patterns are often subjective,...
Zhenjiang Hu, Wei-ngan Chin, Masato Takeichi
The general goal of data mining is to extract interesting correlated information from large collection of data. A key computationally-intensive subproblem of data mining involves nding frequent sets...
A Lazy Divide Conquer Approach to Constraint Solving (2007)
Wei-ngan Chin, Siau-cheng Khoo
Divide and conquer strategy enables a problem to be divided into subproblems, which are solved independently and later combined to form the solutions of the original problem. In solving constraint...
Automated verification of shape and size properties via separation logic (2007)
Huu Hai Nguyen, Cristina David, Shengchao Qin, Wei-ngan Chin
Abstract. Despite their popularity and importance, pointer-based programs remain a major challenge for program verification. In this paper, we propose an automated verification system that is...
Automated verification of shape and size properties via separation logic (2007)
Huu Hai Nguyen, Cristina David, Shengchao Qin, Wei-ngan Chin
Abstract — Despite their popularity and importance, pointerbased programs remain a major challenge for program verification. In this paper, we propose an automated verification system that is...
A flowbased approach for variant parametric types (2006)
Wei-ngan Chin, Florin Craciun, Siau-cheng Khoo, Corneliu Popeea
A promising approach for type-safe generic codes in the objectoriented paradigm is variant parametric type, which allows covariant and contravariant subtyping on fields where appropriate. Previous...
A flowbased approach for variant parametric types (2006)
Wei-ngan Chin, Florin Craciun, Siau-cheng Khoo, Corneliu Popeea
A promising approach for type-safe generic codes in the objectoriented paradigm is variant parametric type, which allows covariant and contravariant subtyping on fields where appropriate. Previous...
Inferring disjunctive postconditions (2006)
Corneliu Popeea, Wei-ngan Chin
Abstract. Polyhedral analysis [9] is an abstract interpretation used for automatic discovery of invariant linear inequalities among numerical variables of a program. Convexity of this abstract domain...
Memory Usage Verification for OO Programs (2005)
Wei-ngan Chin, Huu Hai Nguyen, Shengchao Qin, Martin Rinard
Abstract. We present a new type system for an object-oriented (OO) language that characterizes the sizes of data structures and the amount of heap memory required to successfully execute methods that...
Verifying safety policies with size properties and alias controls (2005)
Wei-ngan Chin, Siau-cheng Khoo, Shengchao Qin, Corneliu Popeea, Huu Hai Nguyen
Many software properties can be analysed through a relational size analysis on each function’s inputs and outputs. Such relational analysis (through a form of dependent typing) has been...
Memory Usage Verification for OO Programs (2005)
Wei-ngan Chin, Huu Hai Nguyen, Shengchao Qin, Martin Rinard
Abstract. We present a new type system for an object-oriented (OO) language that characterizes the sizes of data structures and the amount of heap memory required to successfully execute methods that...
A Type System for Resource Protocol Verification and its Correctness Proof (2004)
Corneliu Popeea, Wei-ngan Chin
We present a new method, based on a form of dependent typing, to verify the correct usage of resources in a program. Our approach allows complex resources to be specified, whose properties are...
A Semantic Foundation for TCOZ in Unifying Theories of Programming Shengchao Qin (2003)
Shengchao Qin, Jin Song Dong, Wei-ngan Chin
Unifying Theories of Programming(UTP) can provide a formal semantic foundation not only for programming languages but also for more expressive specification languages. We believe UTP is particularly...
Deriving pre-conditions for array bound check elimination (2001)
Wei-ngan Chin, Siau-cheng Khoo, Dana N. Xu
Abstract. We present a high-level approach to array bound check optimization that is neither hampered by recursive functions, nor disabled by the presence of partially redundant checks. Our approach...
Deriving pre-conditions for array bound check elimination (2001)
Wei-ngan Chin, Siau-cheng Khoo, Dana N. Xu
We present a high-level approach to array bound check optimization that is neither hampered by recursive functions, nor disabled by the presence of partially redundant checks. Our approach combines a...
Calculating sized types (2000)
Wei-ngan Chin, Siau-cheng Khoo
Abstract. Many program optimizations and analyses, such as array-bounds checking, termination analysis, etc, depend on knowing the size of a function's input and output. However, size...
Calculating Sized Types (2000)
Wei-ngan Chin, Siau-cheng Khoo
Many program optimisations and analyses, such as array-bound checking, termination analysis, etc, depend on knowing the size of a function's input and output. However, size information can be...
Calculating Sized Types (2000)
Wei-ngan Chin, Siau-cheng Khoo
Many program optimisations and analyses, such as arraybound checking, termination analysis, etc, depend on knowing the size of a function's input and output. However, size information can be...
Calculating a New Data Mining Algorithm for Market Basket Analysis (2000)
Zhenjiang Hu, Wei-ngan Chin, Masato Takeichi
. The general goal of data mining is to extract interesting correlated information from large collection of data. A key computationallyintensive subproblem of data mining involves finding frequent...
Calculating a new data mining algorithm for market basket analysis (2000)
Zhenjiang Hu, Wei-ngan Chin, Masato Takeichi
The general goal of data mining is to extract interesting correlated information from large collection of data. A key computationally-intensive subproblem of data mining involves finding frequent...
Deriving parallel codes via invariants (2000)
Wei-ngan Chin, Siau-cheng Khoo, Zhenjiang Hu, Masato Takeichi
Abstract. Systematic parallelization of sequential programs remains a major challenge in parallel computing. Traditional approaches using program schemestendtobenarrower in scope, as the properties...
Effective Optimisation of Multiple Traversals in Lazy Languages (1999)
Wei-ngan Chin, Aik-Hui Goh, Siau-cheng Khoo
Tupling transformation strategy can be applied to eliminate redundant calls in a program and also to eliminate multiple traversals of data structures. While the former application can produce...
A Case Study on a Modular Transformation Strategy (1999)
Zhenjiang Hu, Wei-ngan Chin, Masato Takeichi
this paper, we show that it is possible to minimize these deep insights. Our thesis is that the high-level transformation techniques such as fusion, tupling, and generalization/accumulation can be...
Synchronisation Analysis to Stop Tupling (1998)
Wei-ngan Chin, Siau-cheng Khoo, Tat-wee Lee
. Tupling transformation strategy can be used to merge loops together by combining recursive calls and also to eliminate redundant calls for a class of programs. In the latter case, this...
Parallelization via Context Preservation (1998)
W N Chin, A Takano, Z Hu, Wei-ngan Chin, Akihiko Takano, Zhenjiang Hu
Abstract program schemes, such as scan or homomorphism, can capture a wide range of data parallel programs. While versatile, these schemes are of limited practical use on their own. A key problem is...
Parallelization in Calculational Forms (1998)
Zhenjiang Hu, Masato Takeichi, Wei-ngan Chin
The problems involved in developing efficient parallel programs have proved harder than those in developing efficient sequential ones, both for programmers and for compilers. Although program...
Variable Timestamp-based Distributed Deadlock Detection and Resolution (1997)
Abstract not available.
Enhanced Parallelization via Constraints (1997)
Wei-ngan Chin, Zhenjiang Hu, Masato Takeichi, Akihiko Takano
Systematic parallelization of sequential programs remains a major challenge in parallel computing. Traditional approaches using program schemes are somewhat narrow in scope, as the properties which...
A Modular Derivation Strategy via Fusion and Tupling (1997)
Wei-ngan Chin, Zhenjiang Hu, Masato Takeichi
We show how programming pearls can be systematically derived via fusion, followed by tupling transformations. By focusing on the elimination of intermediate data structures (fusion) followed by the...
Enhanced Parallelization via Constraints (1997)
Wei-ngan Chin, Zhenjiang Hu, Akihiko Takano
Systematic parallelization of sequential programs remains a major challenge in parallel computing. Traditional approaches using program schemes are somewhat narrow in scope, as the properties which...
A Modular Derivation Strategy via Fusion and Tupling (1997)
Wei-ngan Chin, Zhenjiang Hu, Masato Takeichi
We showhow programming pearls can be systematically derived via fusion, followed by tupling transformations. By focusing on the elimination of intermediate data structures #fusion # followed by the...
Variable Timestamp-based Distributed Deadlock Detection and Resolution (1996)
Abstract not available.
Better Consumers for Program Specializations (1996)
Wei-Ngan Chin, Siau-Cheng Khoo, Editorial Board, H. Ait-kaci, L. Augustsson, Ch. Brzoska, ...
It is well known that not all programs are susceptible to automatic program specialization. Traditionally, complicated analyses are performed before actual specialization, in order to uncover as much...
A Transformation Method for Dynamic-Sized Tabulation (1995)
Tupling is a transformation tactic to obtain new functions, without redundant calls and/or multiple traversals of common inputs. It achieves this feat by allowing each set (tuple) of function calls...
Deriving Parallel Codes via Invariants
Wei-ngan Chin, Siau-cheng Khoo, Zhenjiang Hu, Masato Takeichi
. Systematic parallelization of sequential programs remains a major challenge in parallel computing. Traditional approaches using program schemes tend to be narrower in scope, as the properties which...