问SMTChecker在坚固性中的用途是什么？
EN

Ethereum用户

提问于 2019-08-31 09:37:06

回答 1查看 1.7K关注 0票数 8

如果使用pragma experimental SMTChecker;，则会得到其他安全警告，这些警告是通过查询SMT解决程序获得的。该组件还不支持的所有特性，可能会输出许多警告。如果它报告不支持的特性，分析可能不完全正确。

我知道SMT来源于“可满足性模数理论”，但有人能解释这个概念是如何应用于稳健性的吗？这是某种形式的验证吗？

回答已采纳

发布于 2019-08-31 11:32:34

在过于简化的条件下，它是一个内置的形式验证模块的稳健性编译器。

它本质上将程序转换为语句(或者更具体地说，转换为问题)，然后通过返回真值或假值(也被认为是SAT理论中的可满足/不可满足的值)来证明代码是否可以被破坏。

该模块的基本思想是在编译时捕获错误并证明程序的正确性，像这样的模块通常作为编译器优化特性出现，因为它是一种经过数学验证的方法，可以确保行为的一致性，即从高级代码到低级代码的转换过程。

票数 11

页面原文内容由Ethereum提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://ethereum.stackexchange.com/questions/74447

复制

相似问题

问SMTChecker在坚固性中的用途是什么？EN