Conditional quantitative program analysis
File(s)paper.pdf (404.4 KB)
Accepted version
Author(s)
Gerrard, M
Borges, M
Dwyer, M
Fillieri, A
Type
Journal Article
Abstract
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.
Date Issued
2022-04-01
Date Acceptance
2020-08-13
ISSN
0098-5589
Publisher
Institute of Electrical and Electronics Engineers (IEEE)
Start Page
1212
End Page
1227
Journal / Book Title
IEEE Transactions on Software Engineering
Volume
48
Issue
4
Copyright Statement
© 2020 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Identifier
https://ieeexplore.ieee.org/document/9167482
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Engineering, Electrical & Electronic
Computer Science
Engineering
Program analysis
model counting
symbolic execution
conditional analysis
software reliability
software certification
POLYTOPES
ALGORITHM
VOLUME
Software Engineering
0803 Computer Software
0806 Information Systems
0906 Electrical and Electronic Engineering
Publication Status
Published
Date Publish Online
2020-08-14