×

Formal verification of infinite state systems using Boolean methods. (English) Zbl 1151.68473

Pfenning, Frank (ed.), Term rewriting and applications. 17th international conference, RTA 2006, Seattle, WA, USA, August 12–14, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-36834-2/pbk). Lecture Notes in Computer Science 4098, 1-3 (2006).
Summary: Most successful automated formal verification tools are based on a bit-level model of computation, where a set of Boolean state variables encodes the system state. Using powerful inference engines, such as Binary Decision Diagrams (BDDs) and Boolean satisfiability (SAT) checkers, symbolic model checkers and similar tools can analyze all possible behaviors of very large, finite-state systems.
For the entire collection see [Zbl 1113.68009].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

UCLID
PDFBibTeX XMLCite
Full Text: DOI