Please use this identifier to cite or link to this item:
Title: Dual analysis for proving safety and finding bugs
Authors: Popeea, C.
Chin, W.-N. 
Keywords: Automated verification
False positive
Numerical abstract domain
Static analysis
Issue Date: 2013
Citation: Popeea, C., Chin, W.-N. (2013). Dual analysis for proving safety and finding bugs. Science of Computer Programming 78 (4) : 390-411. ScholarBank@NUS Repository.
Abstract: Program bugs remain a major challenge for software developers and various tools have been proposed to help with their localisation and elimination. Most present-day tools are based either on over-approximating techniques that can prove safety but may report false positives, or on under-approximating techniques that can find real bugs but with possible false negatives. In this paper, we propose a dual static analysis that is based only on 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. © 2012 Elsevier B.V. All rights reserved.
Source Title: Science of Computer Programming
ISSN: 01676423
DOI: 10.1016/j.scico.2012.07.004
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.


checked on Oct 17, 2018


checked on Oct 9, 2018

Page view(s)

checked on Oct 20, 2018

Google ScholarTM



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