Please use this identifier to cite or link to this item:
Title: Disjunctive invariants for modular static analysis
Keywords: static analysis, program verification, disjunctive invariants, abstract interpretation, false positives
Issue Date: 22-Jul-2008
Citation: POPEEA CORNELIU CHRISTIAN (2008-07-22). Disjunctive invariants for modular static analysis. ScholarBank@NUS Repository.
Abstract: We study the application of modular static analysis to prove program safety and detection of program errors. The analyses proposed in this thesis benefit from the relationship between a modular analyzer and a precise disjunctive domain. A modular analyzer requires a precise abstract domain to reason about the symbolic method inputs. On the other hand, a modular analyzer has a local scope and therefore favors more complex invariants than those that are usually involved in global analyzers. To handle the challenges of disjunctive analyses, we introduce the notion of affinity to characterize how closely related is a pair of disjuncts. 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.
Appears in Collections:Ph.D Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
popeea.disjunctive-invariants.pdf904.52 kBAdobe PDF



Page view(s)

checked on May 23, 2019


checked on May 23, 2019

Google ScholarTM


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.