问题标签 [formal-verification]

我想在 Z3 中对固定大小的内存缓冲区及其访问操作进行建模。缓冲区的大小可以从几个字节到数百个字节不等。几种现有工具（例如，KLEE）采用的标准方法是在位向量的域和范围内创建数组变量。每个内存缓冲区都有这样一个数组，内存读/写使用select/store操作进行编码。

唉，在我的基准测试中，使用这种方法时，Z3(*) 似乎始终比 STP 慢。在更详细地分析查询以弄清楚发生了什么之前，我想确保我使用“正确”的方法来编码 Z3 中的内存操作（因为，诚然，STP 是专门为与数组和位向量一起使用而设计的）。

那么在 Z3 中表示内存缓冲区的最有效方式是什么？到目前为止，我正在考虑几种替代方案：

1. 使用断言来指定内存缓冲区的初始值，而不是使用嵌套的store-s。但是，在我的初步测试中，这似乎会进一步减慢 Z3 的速度。
2. 使用位向量对缓冲区进行编码。但是，生成的位向量可能会变得非常大（约 1000 位），我不确定 Z3 或任何其他求解器能否有效地处理这个问题。
3. 为每个内存字节创建单独的位向量变量，并使用嵌套ite表达式将内存访问路由到相应的变量。但是，我担心这会使模型变得相当复杂，并引入对量词的需求。
4. 使用未解释的函数而不是数组，但这需要重新定义数组公理，其效率可能低于 Z3 自己的内置数组理论。

我还缺少什么更好的方法吗？

(*) 默认非增量求解器，Z3 分支unstable@aba79802cfb5

我（错误地）学习了一门关于验证并发程序的课程，到目前为止，我们已经介绍了这种称为“Owicki-Gries 方法”的方法。显然，可以通过将断言与每个语句相关联来证明程序的各种结果，并表明这些断言是归纳的并且不会相互干扰。我们的一项任务涉及 Lamports 的快速互斥算法，详见本文：

在论文中，给出了互斥的 Owicki-Gries 风格证明。它看起来完全违反直觉。我很难理解的是如何首先提出这些断言？你什么时候知道这些断言既不是太强（太强以至于它破坏了干涉自由）也不是太弱（例如一些微不足道的东西，比如每个陈述的重言式）？

干杯

测试驱动开发可以正式验证吗？是否可以保证程序正确且正常运行？选择测试有什么正式的依据吗？有什么算法可以遵循吗？

给定一个循环不变量，维基百科列出了一个为循环生成最弱前提条件的好方法（来自http://en.wikipedia.org/wiki/Predicate_transformer_semantics）：

M[x <- N] 用 N 替换 M 中所有出现的 x。

现在，我的问题是变量 y。\forall y, 在表达式中绑定 y，因此“y 是新变量的元组”不会为我解析。\forall 中的 y 是否与 "[x <- y]" 中的 y 相同？我根本无法解析上述内容。

编辑：改写以避免参考请求。

我的问题是：循环不变量和计算最弱前提（如果有的话）之间的直接联系是什么。似乎在实践中所做的很多事情都将循环的最弱前提条件放松为适合验证的前提条件。来自维基百科的上述内容表明，给定一个循环不变量，确实可以计算出鼻子上最弱的先决条件，但我无法理解这个条件。

我在某处读到一个好的规范应该是明确的、完整的和一致的。这些术语的含义是什么？我们怎么能说一个规范是完整的呢？我们怎么能说规范是明确的呢？我们怎么能说一个规范是一致的呢？

提前致谢

我写了一小段 Haskell 来弄清楚 GHC 如何证明对于自然数，你只能将偶数减半：

核心的相关部分变为：

我知道通过 Flip 类型系列的实例转换类型的一般流程，但有些事情我不能完全遵循：

• 是什么意思@~ <Nat.Flip x_apH>_N？是 x 的 Flip 实例吗？这与 有何不同@ (Nat.Flip x_apH)？我既感兴趣< >又_N

关于第一个演员halve：

• 做什么dt_dK6，代表什么？我知道它们是某种等价证明，但哪个是哪个？dt1_dK7dt2_dK8
• 我知道这会Sym向后运行等价
• 是做什么的;？等价证明只是按顺序应用吗？
• 这些_N和_R后缀是什么？
• 是TFCo:R:Flip[0]和TFCo:R:Flip[1]翻转的实例？

它们在 Idris 0.9.14 中实现，我成功地用于induction一些证明。但是，它们仅适用于某些库类型；例如，虽然Vect支持它们，但几乎同构All不支持：

不幸的是，没有大量的语言文档，而且我找不到如何为自定义类型实现消除/案例分析。深入研究 Prelude，我找到了%elim修饰符，但没有帮助。有人可以举个例子All吗？

当我了解concolic 测试的概念时，我遇到了“具体和符号执行”这些术语。（那里提到的文章“CUTE: A concolic unit testing engine for C”在其摘要部分使用了该术语。）

“所使用的方法建立在先前结合符号和具体执行的工作的基础上，更具体地说，使用这种组合来生成测试输入以探索所有可行的执行路径。”

谁能确认“具体执行”是什么意思？尽管我进行了搜索，但我找不到任何直接引用/明确的陈述。

据我了解，“具体执行”是指“执行具有实际输入值的程序，这与符号执行不同，符号执行将符号值假定为变量、输入等”。如果我错了，请纠正我（如果可能的话，举个小例子）。

我正在尝试在 operator和 operator上对我的自定义数据类型Semigroup创建一个和VerifiedSemigroup实例：Bool&&||

所以我首先为over 运算符创建一个命名实例：Semigroup&&

但是在创建VerifiedSemigroup实例时，我如何告诉 Idris 使用 的TodosSemigroup实例Lógico？

该代码给了我以下错误：

详细说明类型时Prelude.Algebra.Main.TodosVerifiedSemigroup，方法semigroupOpIsAssociative：无法解析类型类Semigroup Lógico

如何手动或使用（开源）工具自动将 PSL 或 SVA 活性断言翻译成 verilog？我可以做简单的安全属性，但我对活性属性一无所知。我知道一些商业工具有这个功能来检查 Verilog 设计，但我无权访问它们。

例如，我想将 PSL 中的活性断言翻译assert always req -> eventually! ack;成等效的 Verilog 电路，以便我可以使用一些工具来模型检查该属性是否存在。

• 进行了编辑，将“是否可以翻译...”改写为“我如何翻译”，谢谢 ira！