Sound Probabilistic #SAT with Projection
Logic in Computer Science
2016-10-27 v1 Cryptography and Security
Abstract
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.
Cite
@article{arxiv.1610.08167,
title = {Sound Probabilistic #SAT with Projection},
author = {Vladimir Klebanov and Alexander Weigl and Jörg Weisbarth},
journal= {arXiv preprint arXiv:1610.08167},
year = {2016}
}
Comments
In Proceedings QAPL'16, arXiv:1610.07696