Model-Counting Approaches for Nonlinear Numerical Constraints
Model-Counting Approaches for Nonlinear Numerical Constraints
复制标题
非线性数值约束的模型计数方法
DOI：
10.1007/978-3-319-57288-8_9
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
C. Păsăreanu
中科院分区：
文献类型：
--
作者：
Mateus Borges;Quoc;A. Filieri;C. Păsăreanu
模型计数在系统的定量推理中具有核心重要性。例子包括计算系统成功完成任务而没有错误的概率，以及在香农熵中测量系统泄漏给对手的比特数。大多数以前的工作在这些领域展示了他们的分析程序的线性约束，在这种情况下，模型计数是多项式时间。非线性约束的模型计数是出了名的困难，因此具有非线性约束的程序没有得到很好的研究。本文调查国家的最先进的技术和工具的SMT约束，模的位向量理论模型计数，因为这个理论是可判定的，它可以表示从计算机程序的分析所产生的非线性约束。我们将这些技术集成在Symbolic Pathfinder平台中，并在加密函数分析产生的困难非线性约束上对其进行评估。
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.
DOI：
10.1109/csf.2016.34
发表时间：
2016-08
期刊：
2016 IEEE 29th Computer Security Foundations Symposium (CSF)
影响因子：
--
作者：
C. Păsăreanu;Quoc-Sang Phan;P. Malacaria
通讯作者：
C. Păsăreanu;Quoc-Sang Phan;P. Malacaria