Campus Event Calendar
Event Entry
What and Who
Disjunctive Invariants for Modular Static Analysis
Corneliu Popeea
National University of Singapore
SWS Colloquium
Corneliu Popeea is a PhD candidate in the School of Computing at the
National University of Singapore. He is supervised by Prof Chin
Wei-Ngan. He has received his B.Sc. in computer science from the
University Politehnica of Bucharest (Romania) in 2001. His research
interests lie in programming languages and software engineering. More
specifically, he worked on disjunctive fixed point analysis, inference
of pre/postconditions and type systems for object-oriented languages.
SWS
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 30 June 2008
17:00
60 Minutes
E1 5
Rotunda 6th floor
Saarbrücken
Abstract
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.
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.
Contact
Claudia Richter
9325 688
--email hidden
passcode not visible
logged in users only
Claudia Richter, 06/26/2008 10:23 -- Created document.