Disjunctive Invariants for Modular Static Analysis

  • Corneliu Popeea | National University of Singapore

We study the application of modular static analysis to prove program safety and detection of program errors. In particular, we shall consider imperative programs that rely on numerical invariants.

To handle the challenges of disjunctive analyses, we introduce the notion of affinity to characterize how closely related is a pair of disjuncts. Finding related elements in the conjunctive (base) domain allows the formulation of precise hull and widening operators lifted to the disjunctive (powerset extension of the) base domain. We have implemented a static analyzer based on the disjunctive polyhedral analysis where the relational domain and the proposed operators can progressively enhance precision at a reasonable cost. Our second objective is to support either a proof of the absence of bugs in the case of a valid program or bug finding in the case of a faulty program. We propose a dual static analysis that is designed to track concurrently two over-approximations: the success and the failure outcomes. Due to the concurrent computation of outcomes, we can identify two significant input conditions: a never-bug condition that implies safety for inputs that satisfy it and a must-bug condition that characterizes inputs that lead to true errors in the execution of the program.

Speaker Details

Corneliu Popeea is a PhD student with the Programming Languages group of National University of Singapore, supervised by Professor Chin Wei-Ngan. He has received his B.Sc. in Computer Science in 2001 from Politehnica University of Bucharest, Romania. His research focuses on type-based methods for safe programming, specifically on array bound checks elimination and resource protocol verification.

Watch Next