The Library
Approximate counting in SMT and value estimation for probabilistic programs
Tools
Chistikov, Dmitry, Dimitrova, Rayna and Majumdar, Rupak (2015) Approximate counting in SMT and value estimation for probabilistic programs. In: 21st International Conference, TACAS 2015, London, UK, 11-18 Apr 2015. Published in: Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2015, 9035 pp. 320-334. doi:10.1007/978-3-662-46681-0_26 ISSN 0302-9743.
Research output not available from this repository.
Request-a-Copy directly from author or use local Library Get it For Me service.
Official URL: http://dx.doi.org/10.1007/978-3-662-46681-0_26
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 version of #SMT to SMT.
We focus on the theories of integer arithmetic and linear real arithmetic. We propose model counting algorithms that provide approximate solutions with formal bounds on the approximation error. They run in polynomial time and make a polynomial number of queries to the SMT solver for the underlying theory, exploiting “for free” the sophisticated heuristics implemented within modern SMT solvers. We have implemented the algorithms and used them to solve a value estimation problem for a model of loop-free probabilistic programs with nondeterminism.
Item Type: | Conference Item (Paper) | ||||
---|---|---|---|---|---|
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||
Series Name: | Theoretical Computer Science and General Issues | ||||
Journal or Publication Title: | Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2015 | ||||
Publisher: | Springer | ||||
ISSN: | 0302-9743 | ||||
Book Title: | Tools and Algorithms for the Construction and Analysis of Systems | ||||
Official Date: | 2015 | ||||
Dates: |
|
||||
Volume: | 9035 | ||||
Page Range: | pp. 320-334 | ||||
DOI: | 10.1007/978-3-662-46681-0_26 | ||||
Status: | Peer Reviewed | ||||
Publication Status: | Published | ||||
Access rights to Published version: | Restricted or Subscription Access | ||||
Conference Paper Type: | Paper | ||||
Title of Event: | 21st International Conference, TACAS 2015 | ||||
Type of Event: | Conference | ||||
Location of Event: | London, UK | ||||
Date(s) of Event: | 11-18 Apr 2015 |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |