Statistical Reachability Analysis

Abstract

Given a target program state (or statement) s, what is the probability that an input reaches s? This is the quantitative reachability analysis problem. For instance, quantitative reachability analysis can be used to approximate the reliability of a program (where s is a bad state). Traditionally, quantitative reachability analysis is solved as a model counting problem for a formal constraint that represents the (approximate) reachability of s along paths in the program, i.e., probabilistic reachability analysis. However, in preliminary experiments, we failed to run state-of-the-art probabilistic reachability analysis on reasonably large programs.

BibTeX

@inproceedings{Lee-Boehme:FSE23,
  author    = {Seongmin Lee and
               Marcel B{\"{o}}hme},
  title     = {Statistical Reachability Analysis},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {326--337},
  publisher = {{ACM}},
  year      = {2023},
}

Statistical Reachability Analysis

Abstract

Related papers