@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@inproceedings{fremont-smt14,
  author    = {Daniel J. Fremont and Sanjit A. Seshia},
  title     = {Speeding Up SMT-Based Quantitative Program Analysis},
 booktitle = {In 12th International Workshop on Satisfiability Modulo Theories (SMT)},
 month = "July",
 year = {2014},
 pages = {3--13},
 abstract = {Quantitative program analysis involves computing numerical quantities about individual or collections 
of program executions. An example of such a computation is quantitative information flow 
analysis, where one estimates the amount of information leaked about secret data through a program's
output channels. Such information can be quantified in several ways, including channel capacity and 
(Shannon) entropy. In this paper, we formalize a class of quantitative analysis problems defined over 
a weighted control flow graph of a loop-free program. These problems can be solved using a combination 
of path enumeration, SMT solving, and model counting. However, existing methods can only 
handle very small programs, primarily because the number of execution paths can be exponential in 
the program size. We show how path explosion can be mitigated in some practical cases by taking advantage 
of special branching structure and by novel algorithm design. We demonstrate our techniques 
by computing the channel capacities of the timing side-channels of two programs with extremely large 
numbers of paths.},
}