×

Dual analysis for proving safety and finding bugs. (English) Zbl 1264.68065

Summary: 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.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

DART; BLAST; ESC/Java; GHC
Full Text: DOI