verifiable-c
-
在带有 VST 的 semax 上下文中使用 sep_apply
-
Verifiable-C 支持 C 的哪个子集？
-
在 VST 中验证具有异构数组的程序
-
VST forward_call 非标准调用约定失败
-
Coq VST 内部结构复制
-
为什么 while 循环基于类型检查 (w/ tc_expr) 条件表达式？
-
具有可寻址局部变量的规范
-
寻找指定功能规范 Verifiable-c 的方法
-
前提条件中的数组范围
-
如何在函数规范中使用超过 8 个变量？
-
如何对持有 return 值的变量使用 retval-postcondition？
-
如何在 VST 中处理 "Forall (closed_wrt_vars (eq _z')) P " 个目标？
-
semax_func_cons - 没有适用的策略
-
证明数组存储时的奇怪 VST 目标
-
PLCC 书。第 23 页。是否印刷错误，是否应将 sigma 替换为 sigma prime？
-
如何推理 VST 中的数组访问？