Critical software should be verified. But how to handle the situation when a proof of 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 talk, we present our work on the quantification of C program reliability. Our formal approach measures the reliability of a program in terms of its adherence to a provided functional specification. Our implementation can handle bounded C programs precisely where the functionality is specified through assumptions and assertions in the source code. Following a preparatory program transformation, we use a combination of techniques for software bounded model checking and model counting to obtain quantitative results. This approach allows us to count and categorize the possible runs of the software, permitting the computation of the software's reliability as the share of failing program runs. We evaluated our implementation on a representative set of 24 (deterministic and non-deterministic) C programs and showed differences in performance between an exact and an approximate model counter. The evaluation also led to the publication of a total of 123 benchmark instances for projected model counting.

After summarizing the results of our paper, we briefly present future pathways to increase the efficiency and applicability of our approach.