formal-verification
-
无法证明仅依赖 Implementations/Inlining 的基本功能
-
TLA+ 中的咖啡罐问题：无法表达任务
-
在 Dafny 链表实现中使用空引用终止循环
-
交换数组索引 SPARK-Ada 中的潜在别名冲突
-
为什么 TLC 在有效状态上报告错误？
-
您如何证明一个简单的无意义代码是否可计算？
-
为什么不推断出这个愚蠢的post-条件？
-
如何根据 Coq 中的规范构建字节列表
-
如果在 Coq 中两个归纳类型的构造函数表达式相等，我可以根据它们对应的参数进行重写吗？
-
考虑到我对列表的索引范围的约束，我可以在这里使用 destruct 吗？
-
Coq error: Unable to unify "true" with "is_true (0 < a - b - 3)"
-
Coq 中是否有任何策略可以将 bool 表达式转换为 Prop 表达式？
-
不变量失败但在循环验证之前断言
-
将引理应用于合取分支而不在 coq 中拆分
-
量化权限和通配符的预期错误或不完整？
-
使用Isabelle's theorem prover 证明的过程是在编程模式下编码，然后在证明模式下验证吗？
-
如何快速入门Isabelle的形式化语言标准来形式化描述建模语言？
-
VST forward_call 非标准调用约定失败
-
如何在 Isabelle 中证明这个简单的定理？
-
在 Coq 中提供示例，其中 (A B: Prop)，P: Prop -> Type，这样 A <-> B，但不能用 P B 替换 P A