形式验证里的cutpoint怎么理解

海狸先生0119 · 发表于 2022-3-18 10:05:04

您需要登录才可以下载或查看，没有账号？注册

×

形式验证里的cutpoint怎么理解?在什么情况下需要设置cutpoint相关变量？
谢谢。

xiaofei_heu · 发表于 2025-2-20 15:06:56

一般简化形式验证的逻辑空间时会设置cutpoint,当一个点设置了cutpoint后，与该点相关的property的运算空间就会大大减小，增加了形式验证工具的可用性

songzijian87 · 发表于 2025-3-31 16:51:20

xiaofei_heu 发表于 2025-2-20 15:06
一般简化形式验证的逻辑空间时会设置cutpoint,当一个点设置了cutpoint后，与该点相关的property的运算空间 ...

赞同这个说法，详见下图

账号		自动登录	找回密码
密码			注册

[求助] 形式验证里的cutpoint怎么理解