Formal Verification of Infinite State Systems Using Boolean Methods

Author

Bryant, Randal E.

Author_Institution

Sch. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA

fYear

0

fDate

0-0 0

Firstpage

3

Lastpage

4

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 finite-state 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

Keywords

Boolean functions; automata theory; computability; formal verification; Boolean methods; Boolean satisfiability solver; UCLID modeling language; decision procedure; equisatisfiable Boolean formula; formal verification; hardware designs; infinite state systems; quantifier-free formula; safety properties; Automation; Boolean functions; Computer science; Data structures; Formal verification; Hardware; Logic; Power system modeling; Protocols; Safety;

fLanguage

English

Publisher

ieee

Conference_Titel

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

Conference_Location

Seattle, WA

ISSN

1043-6871

Print_ISBN

0-7695-2631-4

Type

conf

DOI

10.1109/LICS.2006.27

Filename

1691211