Wei Ngan Chin
Email Address
dcscwn@nus.edu.sg
87 results
Publication Search Results
Now showing 1 - 10 of 87
Publication Foreword(2014) Chin, W.-N.; Hage, J.; COMPUTER SCIENCEPublication Enhancing modular OO verification with separation logic(2008) Chin, W.-N.; David, C.; Nguyen, H.H.; Qin, S.; COMPUTER SCIENCEConventional specifications for object-oriented (OO) programs must adhere to behavioral subtyping in support of class inheritance and method overriding. However, this requirement inherently weakens the specifications of overridden methods in superclasses, leading to imprecision during program reasoning. To address this, we advocate a fresh approach to OO verification that focuses on the distinction and relation between specifications that cater to calls with static dispatching from those for calls with dynamic dispatching. We formulate a novel specification subsumption that can avoid code re-verification, where possible. Using a predicate mechanism, we propose a flexible scheme for supporting class invariant and lossless casting. Our aim is to lay the foundation for a practical verification system that is precise, concise and modular for sequential OO programs. We exploit the separation logic formalism to achieve this. © 2008 ACM.Publication Immutable specifications for more concise and precise verification(2011) David, C.; Chin, W.-N.; COMPUTER SCIENCEIn the current work, we investigate the benefits of immutability guarantees for allowing more flexible handling of aliasing, as well as more precise and concise specifications. Our approach supports finer levels of control that can mark data structures as being immutable through the use of immutability annotations. By using such annotations to encode immutability guarantees, we expect to obtain better specifications that can more accurately describe the intentions, as well as prohibitions, of the method. Ultimately, our goal is improving the precision of the verification process, as well as making the specifications more readable, more precise and as an enforceable program documentation.We have designed and implemented a new entailment procedure to formally and automatically reason about immutability enhanced specifications. We have also formalised the soundness for our new procedure through an operational semantics with mutability assertions on the heap. Lastly, we have carried out a set of experiments to both validate and affirm the utility of our current proposal on immutability enhanced specification mechanism. Copyright is held by the author / owner(s).Publication Memory usage verification using Hip/Sleek(2009) He, G.; Qin, S.; Luo, C.; Chin, W.-N.; COMPUTER SCIENCEEmbedded systems often come with constrained memory footprints. It is therefore essential to ensure that software running on such platforms fulfils memory usage specifications at compile-time, to prevent memory-related software failure after deployment. Previous proposals on memory usage verification are not satisfactory as they usually can only handle restricted subsets of programs, especially when shared mutable data structures are involved. In this paper, we propose a simple but novel solution. We instrument programs with explicit memory operations so that memory usage verification can be done along with the verification of other properties, using an automated verification system Hip/Sleek developed recently by Chin et al.[10,19]. The instrumentation can be done automatically and is proven sound with respect to an underlying semantics. One immediate benefit is that we do not need to develop from scratch a specific system for memory usage verification. Another benefit is that we can verify more programs, especially those involving shared mutable data structures, which previous systems failed to handle, as evidenced by our experimental results. © 2009 Springer-Verlag Berlin Heidelberg.Publication An expressive framework for verifying deadlock freedom(2013) Le, D.-K.; Chin, W.-N.; Teo, Y.-M.; COMPUTER SCIENCEThis paper presents an expressive specification and verification framework for ensuring deadlock freedom of shared-memory concurrent programs that manipulate locks. We introduce a novel delayed lockset checking technique to guarantee deadlock freedom of programs with interactions between thread and lock operations. With disjunctive formulae, we highlight how an abstraction based on precise lockset can be supported in our framework. By combining our technique with locklevels, we form a unified formalism for ensuring deadlock freedom from (1) double lock acquisition, (2) interactions between thread and lock operations, and (3) unordered locking. The proposed framework is general, and can be integrated with existing specification logics such as separation logic. Specifically, we have implemented this framework into a prototype tool, called ParaHIP, to automatically verify deadlock freedom and correctness of concurrent programs against user-supplied specifications. © 2013 Springer International Publishing.Publication Proceedings for FTfJP 2012: The 14th Workshop on Formal Techniques for Java-Like Programs - Co-located with ECOOP 2012 and PLDI 2012, Papers Presented at the Workshop: Foreword(2012) Chin, W.-N.; Hobor, A.; COMPUTER SCIENCEPublication A higher-order removal method(1996) Chin, W.-N.; Darlington, J.; INFORMATION SYSTEMS & COMPUTER SCIENCEA major attraction of functional languages is their support for higher-order functions. This facility increases the expressive power of functional languages by allowing concise and reusable programs to be written. However, higher-order functions are more expensive to execute and to analyse for optimisations. To reduce the performance penalties of using higher-order functions, this paper proposes two transformation algorithms which could automatically remove most higher-order functions from functional programs. The first algorithm uses an eta-expansion technique to eliminate expressions which return function-type results. The second algorithm uses & function specialisation technique to eliminate expressions with function-type arguments. Together, they remove higher-order functions by transforming each higher-order program to an equivalent firstorder (or lower-order) program. We shall prove that the two algorithms are terminating (when applied to well-typed programs) and also totally-correct (preserving non-strict semantics). © 1996 Kluwer Academic Publishers,.Publication Automated verification of shape, size and bag properties(2007) Chin, W.-N.; David, C.; Nguyen, H.H.; Qin, S.; COMPUTER SCIENCEIn recent years, separation logic has emerged as a contender for formal reasoning of heap-manipulating imperative programs. Recent works have focused on specialised provers that are mostly based on fixed sets of predicates. To improve expressivity, we have proposed a prover that can automatically handle user-defined predicates. These shape predicates allow programmers to describe a wide range of data structures with their associated size properties. In the current work, we shall enhance this prover by providing support for a new type of constraints, namely bag (multiset) constraints. With this extension, we can capture the reachable nodes (or values) inside a heap predicate as a bag constraint. Consequently, we are able to prove properties about the actual values stored inside a data structure. © 2007 IEEE.Publication An automatic mapping from Statecharts to Verilog(2005) Tran, V.-A.V.; Qin, S.; Chin, W.N.; SINGAPORE-MIT ALLIANCE; COMPUTER SCIENCEStatecharts is a visual formalism suitable for high-level system specification, while Verilog is a hardware description language that can be used for both behavioural and structural specification of (hardware) systems. This paper implements a semantics-preserving mapping from Graphical Statecharts to Verilog programs, which, to the best of our knowledge, is the first algorithm to bridge the gap between Statecharts and Verilog, and can be embedded into the hardware/software co-specification process [19] as a front-end. © Springer-Verlag Berlin Heidelberg 2005.Publication Loop invariant synthesis in a combined abstract domain(2013) Qin, S.; He, G.; Luo, C.; Chin, W.-N.; Chen, X.; COMPUTER SCIENCEAutomated verification of memory safety and functional correctness for heap-manipulating programs has been a challenging task, especially when dealing with complex data structures with strong invariants involving both shape and numerical properties. Existing verification systems usually rely on users to supply annotations to guide the verification, which can be cumbersome and error-prone by hand and can significantly restrict the usability of the verification system. In this paper, we reduce the need for some user annotations by automatically inferring loop invariants over an abstract domain with both shape and numerical information. Our loop invariant synthesis is conducted automatically by a fixed-point iteration process, equipped with newly designed abstraction mechanism, together with join and widening operators over the combined domain. We have also proven the soundness and termination of our approach. Initial experiments confirm that we can synthesise loop invariants with non-trivial constraints. © 2012 Elsevier B.V.