Dual analysis for proving safety and finding bugs

Program bugs remain a major challenge for software developers and various tools have been proposed to help with their localization and elimination. Most present-day tools are based either on over-approximating techniques that can prove safety but may report false positives, or on underapproximating techniques that can find real bugs but with possible false negatives. In this paper, we propose a dual static analysis that is based on only over-approximation. Its main novelty is to concurrently derive conditions that lead to either success or failure outcomes and thus we provide a comprehensive solution for both proving safety and finding real program bugs. We have proven the soundness of our approach and have implemented a prototype system that is validated by a set of experiments. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; F.3.2 [Logics...

• Type: Conference
• Year: 2010
• Where: SAC
• Authors: Corneliu Popeea, Wei-Ngan Chin
• Keywords: Applied Computing, Most Present-day Tools, Program Bugs, SAC 2010, Static Analysis