Paper 2017/244

Model-counting Approaches For Nonlinear Numerical Constraints

Mateus Borges, Quoc-Sang Phan, Antonio Filieri, and Corina S. Păsăreanu


Model counting is of central importance in quantitative reasoning about systems. Examples include computing the probability that a system successfully accomplishes its task without errors, and measuring the number of bits leaked by a system to an adversary in Shannon entropy. Most previous work in those areas demonstrated their analysis on programs with linear constraints, in which cases model counting is polynomial time. Model counting for nonlinear constraints is notoriously hard, and thus programs with nonlinear constraints are not well-studied. This paper surveys state-of-the-art techniques and tools for model counting with respect to SMT constraints, modulo the bitvector theory, since this theory is decidable, and it can express nonlinear constraints that arise from the analysis of computer programs. We integrate these techniques within the Symbolic Pathfinder platform and evaluate them on difficult nonlinear constraints generated from the analysis of cryptographic functions.

Available format(s)
Publication info
Published elsewhere. MAJOR revision.9th NASA Formal Methods Symposium NFM 2017
Side-channel AttacksModulo ExponentiationQuantitative Information FlowModel Counting Modulo Theories
Contact author(s)
sang phan @ sv cmu edu
2017-03-20: received
Short URL
Creative Commons Attribution


      author = {Mateus Borges and Quoc-Sang Phan and Antonio Filieri and Corina S.  Păsăreanu},
      title = {Model-counting Approaches For Nonlinear Numerical Constraints},
      howpublished = {Cryptology ePrint Archive, Paper 2017/244},
      year = {2017},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.