Journal article icon

Journal article

Approximate counting in SMT and value estimation for probabilistic programs

Abstract:

#SMT, or model counting for logical theories, is a well-known hard problem that generalizes such tasks as counting the number of satisfying assignments to a Boolean formula and computing the volume of a polytope. In the realm of satisfiability modulo theories (SMT) there is a growing need for model counting solvers, coming from several application domains (quantitative information flow, static analysis of probabilistic programs). In this paper, we show a reduction from an approximate versi...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed

Actions


Access Document


Files:
Publisher copy:
10.1007/s00236-017-0297-2

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author
Publisher:
Springer
Journal:
Acta Informatica More from this journal
Volume:
54
Issue:
8
Pages:
729–764
Publication date:
2017-04-12
Acceptance date:
2017-03-16
DOI:
EISSN:
1432-0525
ISSN:
0001-5903
Keywords:
Pubs id:
pubs:687611
UUID:
uuid:90901b5e-3244-4306-9336-156a935414f9
Local pid:
pubs:687611
Source identifiers:
687611
Deposit date:
2017-03-30

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP