Standards for certifying safety-critical systems have evolved to permit the inclusion of evidence generated by program analysis and verification techniques. The past decade has witnessed the development of several program analyses that are capable of computing guarantees on bounds for the probability of failure. This paper develops a novel program analysis framework, CQA, that combines evidence from different underlying analyses to compute bounds on failure probability. It reports on an evaluation of different CQA-enabled analyses and implementations of state-of-the-art quantitative analyses to evaluate their relative strengths and weaknesses. To conduct this evaluation, we filter an existing verification benchmark to reflect certification evidence generation challenges. Our evaluation across the resulting set of 136 C programs, totaling more than 385k SLOC, each with a probability of failure below$10^{-4}$, demonstrates how CQA extends the state-of-the-art. The CQA infrastructure, including tools, subjects, and generated data is publicly available atbitbucket.org/mgerrard/cqa.

There is often more than one way to trigger a fault. Standard static and dynamic approaches focus on exhibiting a single witness for a failing execution. In this paper, we study the problem of computing a comprehensive characterization which safely bounds all failing program behavior while exhibiting a diversity of witnesses for those failures. This information can be used to facilitate software engineering tasks ranging from fault localization and repair to quantitative program analysis for reliability. Our approach combines the results of overapproximating and underapproximating static analyses in an alternating iterative framework to produce upper and lower bounds on the failing input space of a program, which we call a comprehensive failure characterization (CFC). We evaluated a prototype implementation of this alternating framework on a set of 168 C programs from the SV-COMP benchmarks, and the data indicate that it is possible to efficiently, accurately, and safely characterize failure spaces.