Skip to main content
SpringerLink
Log in

Formal Verification of Infinite State Systems Using Boolean Methods

  • Conference paper
Term Rewriting and Applications (RTA 2006)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4098))

Included in the following conference series:

  • 363 Accesses

Abstract

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.

This research was supported by the Semiconductor Research Corporation, Contract RID 1029.001.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 78–92. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  2. Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Convergence testing in term-level bounded model checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 348–362. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  3. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages (POPL 1977), pp. 238–252 (1977)

    Google Scholar 

  4. Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)

    Google Scholar 

  5. Lahiri, S.K., Bryant, R.E.: Indexed predicate discovery for unbounded system verification. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 135–147. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  6. Lahiri, S.K., Bryant, R.E.: Indexed predicate abstraction. In: ACM Transactions on Computational Logic (to appear)

    Google Scholar 

  7. Lahiri, S.K., Seshia, S.A.: The UCLID decision procedure. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 475–478. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  8. Lahiri, S.K., Seshia, S.A., Bryant, R.E.: Modeling and verification of out-of-order microprocessors in UCLID. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 142–159. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  9. McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1992)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, Carnegie Mellon University, Pittsburgh, PA

    Randal E. Bryant

Authors
  1. Randal E. Bryant
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Carnegie Mellon University,  

    Frank Pfenning

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bryant, R.E. (2006). Formal Verification of Infinite State Systems Using Boolean Methods. In: Pfenning, F. (eds) Term Rewriting and Applications. RTA 2006. Lecture Notes in Computer Science, vol 4098. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11805618_1

Download citation

  • DOI: https://doi.org/10.1007/11805618_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-36834-2

  • Online ISBN: 978-3-540-36835-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation