| Abstract |
|
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 finitestate
systems. The UCLID modeling language describes
systems where the state variables are Booleans, integers,
and functions mapping integers to integers or Booleans.
The verifier supports several forms of verification for proving
safety properties. They rely on a decision procedure that
translates a quantifier-free formula into an equi-satisfiable
Boolean formula and then applies a Boolean satisfiability
solver. UCLID has successfully verified a number of hardware
designs and protocols.
|
 Additional Information
|
Citation:
Randal E. Bryant,
"Formal Verification of Infinite State Systems Using Boolean Methods,"
lics,
pp. 3-4,
21st Annual IEEE Symposium on Logic in Computer Science (LICS'06),
2006
|
