This project studied the application of procedure-modular static analysis for verification of sequential programs. A first contribution is the notion of affinity used to characterize how closely related is a pair of disjuncts during program analysis via abstract interpretation [1]. This lead to the design of a novel disjunctive numerical abstract domain that was used to compute precise (weak) method preconditions [2] and precise (strong) method postconditions [1]. We used the disjunctive abstract domain for a static analysis to estimate upper-bounds on the memory consumption of bytecode programs [3]. To filter automatically false positives raised by static analysis, we proposed a dual static analysis [5,6].
This project has been carried mostly at the National University of Singapore and is joint work with my PhD advisor, Wei-Ngan Chin. The paper [2] is co-authored with Dana Xu. The paper [3] is co-authored with Huu Hai Nguyen and Shengchao Qin.