Sound Probabilistic #SAT with Projection
Vladimir Klebanov, Alexander Weigl, Jörg Weisbarth · Electronic Proceedings in Theoretical Computer Science · 2016
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.