Model Counting, Uniform Generation, and Quantitative Information Flow
Supratik Chakraborty, Daniel J. Fremont, Kuldeep Meel, Sanjit Seshia, Moshe Vardi

Citation
Supratik Chakraborty, Daniel J. Fremont, Kuldeep Meel, Sanjit Seshia, Moshe Vardi. "Model Counting, Uniform Generation, and Quantitative Information Flow". Talk or presentation, 29, October, 2014.

Abstract
Model counting is a generalization of SAT which asks not just whether a propositional formula has a satisfying assignment, but how many such assignments there are. This problem and the closely related one of generating satisfying assignments uniformly at random have a wide variety of applications including probabilistic inference, Monte Carlo simulation, and constrained-random verification. In particular, model counting is an essential tool for quantitative information flow analysis, which seeks to measure how much information is leaked by a program. In this poster we describe two lines of research we have been working on lately. First, we have improved recent approximate model counting and sampling algorithms by Chakraborty et al., making them more performant and extending them to the case where assignments have unequal weights. Second, we have developed a new technique for QIF analysis of timing and power side-channels in programs with certain types of control flow that were difficult for earlier methods to handle.

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Supratik Chakraborty, Daniel J. Fremont, Kuldeep Meel,
  Sanjit Seshia, Moshe Vardi. <a
  href="http://www.terraswarm.org/pubs/407.html"
  ><i>Model Counting, Uniform Generation, and
  Quantitative Information Flow</i></a>, Talk or
  presentation,  29, October, 2014.

• Plain text

  Supratik Chakraborty, Daniel J. Fremont, Kuldeep Meel,
  Sanjit Seshia, Moshe Vardi. "Model Counting, Uniform
  Generation, and Quantitative Information Flow". Talk or
  presentation,  29, October, 2014.

• BibTeX

  @presentation{ChakrabortyFremontMeelSeshiaVardi14_ModelCountingUniformGenerationQuantitativeInformation,
      author = {Supratik Chakraborty and Daniel J. Fremont and
                Kuldeep Meel and Sanjit Seshia and Moshe Vardi},
      title = {Model Counting, Uniform Generation, and
                Quantitative Information Flow},
      day = {29},
      month = {October},
      year = {2014},
      abstract = {Model counting is a generalization of SAT which
                asks not just whether a propositional formula has
                a satisfying assignment, but how many such
                assignments there are. This problem and the
                closely related one of generating satisfying
                assignments uniformly at random have a wide
                variety of applications including probabilistic
                inference, Monte Carlo simulation, and
                constrained-random verification. In particular,
                model counting is an essential tool for
                quantitative information flow analysis, which
                seeks to measure how much information is leaked by
                a program. In this poster we describe two lines of
                research we have been working on lately. First, we
                have improved recent approximate model counting
                and sampling algorithms by Chakraborty et al.,
                making them more performant and extending them to
                the case where assignments have unequal weights.
                Second, we have developed a new technique for QIF
                analysis of timing and power side-channels in
                programs with certain types of control flow that
                were difficult for earlier methods to handle.},
      URL = {http://terraswarm.org/pubs/407.html}
  }
  

Posted by Daniel J. Fremont on 28 Oct 2014.
Groups: tools