
handle: 10044/1/83791
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 104 , demonstrates how CQA extends the state-of-the-art. The CQA infrastructure, including tools, subjects, and generated data is publicly available at bitbucket.org/mgerrard/cqa.
Technology, Science & Technology, conditional analysis, software certification, Program analysis, Software Engineering, 0803 Computer Software, Engineering, Electrical & Electronic, software reliability, Computer Science, Software Engineering, 004, 0906 Electrical and Electronic Engineering, Engineering, 0806 Information Systems, Computer Science, VOLUME, Electrical & Electronic, ALGORITHM, symbolic execution, POLYTOPES, model counting
Technology, Science & Technology, conditional analysis, software certification, Program analysis, Software Engineering, 0803 Computer Software, Engineering, Electrical & Electronic, software reliability, Computer Science, Software Engineering, 004, 0906 Electrical and Electronic Engineering, Engineering, 0806 Information Systems, Computer Science, VOLUME, Electrical & Electronic, ALGORITHM, symbolic execution, POLYTOPES, model counting
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 2 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
