Model-counting approaches for nonlinear numerical constraints
File(s)
Accepted version
Author(s)
Borges, M
Phan, QS
Filieri, A
Pasareanu, CS
Type
Conference Paper
Abstract
Model counting is of central importance in quantitative rea-
soning 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 pro-
grams 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.
soning 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 pro-
grams 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.
Date Issued
2017-01-01
Date Acceptance
2017-02-04
Citation
Lecture Notes in Computer Science, 10227
ISBN
9783319572871
ISSN
0302-9743
Publisher
Springer
Journal / Book Title
Lecture Notes in Computer Science
Volume
10227
Copyright Statement
© Springer International Publishing AG 2017. The final authenticated version is available online at https://doi.org/10.1007/978-3-319-57288-8_9
Source
NASA Formal Methods Symposium 2017
Subjects
08 Information And Computing Sciences
Artificial Intelligence & Image Processing
Publication Status
Published
Start Date
2017-05-16
Finish Date
2017-05-18
Coverage Spatial
Moffett Field, CA, USA
Date Publish Online
2017-04-09