Sound Probabilistic #SAT with Projection
This work addresses the need for accurate probabilistic methods in program analysis, particularly for security and resource consumption, but appears incremental as it builds on existing techniques.
The paper tackles the problem of sound probabilistic estimation of the model count for boolean formulas under projection, with applications in quantitative program analyses like information flow quantification.
We present an improved method for a sound probabilistic estimation of the model count of a boolean formula under projection. The problem solved can be used to encode a variety of quantitative program analyses, such as concerning security of resource consumption. We implement the technique and discuss its application to quantifying information flow in programs.