为组合验证生成自动化假设的方法、系统和计算机程序产品

摘要

本发明涉及为组合验证生成自动化假设的方法、系统和计算机程序产品。公开了一种用于计算精确的最小自动机以担当假设-保证推理中的中间断言的方法、系统和计算机程序产品。在一个实施例中，通过使用采样方法和布尔可满足性来执行对精确最小自动机的计算。这里所描述的方法可以被用作形式验证工具的一部分。