Invited Paper: Formal Verification of Infinite State Systems Using Boolean Methods (at LICS 2006)

Authors: Randal E. Bryant

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.

BibTeX

  @InProceedings{Bryant-FormalVerificationo,
    author = 	 {Randal E. Bryant},
    title = 	 {Formal Verification of Infinite State Systems Using Boolean Methods},
    booktitle =  {Proceedings of the Twenty-First Annual IEEE Symposium on Logic in Computer Science (LICS 2006)},
    year =	 {2006},
    month =	 {August}, 
    pages =      {3--4},
    location =   {Seattle, Washington, USA}, 
    note =       {Invited Talk},
    publisher =	 {IEEE Computer Society Press}
  }