@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@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},
note = "To appear.",
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.},
}