Disjunctive invariants for modular verification

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].

  1. ASIAN 2006 Inferring Disjunctive Postconditions (pdf) (slides)
  2. PEPM 2008 A Practical and Precise Inference and Specializer for Array Bound Checks Elimination (pdf) (slides)
  3. ISMM 2008 Analysing Memory Resource Bounds for Low-Level Programs (pdf) (slides)
  4. PhD-thesis 2008 Disjunctive Invariants for Modular Static Analysis (pdf)
  5. SAC 2010 Dual analysis for proving safety and finding bugs (pdf) (slides) (project webpage)
  6. SCP 2012 Dual analysis for proving safety and finding bugs (pdf)

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.