Quantifying Software Reliability via Model-Counting
Critical software should be verified. But how to handle the situation when a proof for the functional correctness could not be established? In this case, an assessment of the software is required to estimate the risk of using the software. In this paper, we contribute to the assessment of critical software with a formal approach to measure the reliability of the software against its functional specification. We support bounded C-programs precisely where the functional specification is given as assumptions and assertions within the source code. We count and categorize the various program runs to compute the reliability as the ratio of failing program runs (violating an assertion) to all terminating runs. Our approach consists of a preparing program translation, the reduction of C-program into SAT instances via software-bounded model-checker (cbmc), and precise or approximate model-counting providing a reliable assessment. We evaluate our prototype implementation on over 24 examples with different model-counters. We show the feasibility of our pipeline and benefits against competitors.
Code (1)
Tasks
modelSimilar Papers 제목 키워드 기반
A Study of the Learnability of Relational Properties: Model Counting Meets Machine Learning (MCML)
This paper introduces the MCML approach for empirically studying the learnability of relational properties that can be expressed in the well-known software design language Alloy. A key novelty of MCML is quantification o…
BIG-bench Machine LearningMulti-source Multi-scale Counting in Extremely Dense Crowd Images
We propose to leverage multiple sources of information to compute an estimate of the number of individuals present in an extremely dense crowd visible in a single image. Due to problems including perspective, occlusion, …
Crowd CountingHuman DetectionAlgebraic Model Counting for Global Analysis of Optimal Decision Trees
Ensuring model reliability in Explainable AI requires a global assessment of the hypothesis space. We propose a formal framework for the exhaustive analysis of optimal and near-optimal decision trees, called Algebraic De…
Counting Hallucinations in Diffusion Models
Diffusion probabilistic models (DPMs) have demonstrated remarkable progress in generative tasks, such as image and video synthesis. However, they still often produce hallucinated samples (hallucinations) that conflict wi…
Image GenerationModelling Open-Source Software Reliability Incorporating Swarm Intelligence-Based Techniques
In the software industry, two software engineering development best practices coexist: open-source and closed-source software. The former has a shared code that anyone can contribute, whereas the latter has a proprietary…
parameter estimation