Formal verification of infinite state systems using Boolean methods

被引：0

作者：

Bryant, Randal E. ^{[1
]}

机构：

[1] Carnegie Mellon Univ, Sch Comp Sci, Pittsburgh, PA 15213 USA

来源：

21st Annual IEEE Symposium on Logic in Computer Science, Proceedings | 2006年

关键词：

D O I：

10.1109/LICS.2006.27

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

The UCLID project seeks to develop formal verification tools for infinite-state systems having a degree of automation comparable to that of model checking tools for finite-state systems. Yhe UCLID modeling language describes systems where the state variables are Booleans, integers, and functions mapping integers to integers or Booleans. The verifier supports severalforms of verification for proving safety properties. They rely on a decision procedure that translates a quantifier-freeformula into an equi-satisfiable Boolean formula and then applies a Boolean satisfiability solver UCLID has successfully verified a number of hardware designs and protocols.

引用

页码：3 / 4

页数：2