Sound Probabilistic #SAT with Projection

Vladimir Klebanov
(KIT)
Alexander Weigl
(KIT)
Jörg Weisbarth

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.

In Mirco Tribastone and Herbert Wiklicky: Proceedings 14th International Workshop Quantitative Aspects of Programming Languages and Systems (QAPL'16), Eindhoven, The Netherlands, April 2-3, 2016, Electronic Proceedings in Theoretical Computer Science 227, pp. 15–29.
Published: 25th October 2016.

ArXived at: https://dx.doi.org/10.4204/EPTCS.227.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org