Abstract
We present an inductive characterization for an invariant to stand in a given finite-state transition system. We show how this characterization can be computed by means of BDD-based operations, without performing a fixpoint iteration over sets of states as the CTL symbolic model checking algorithm does.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Anderson, R. J., Beame, P., Burns, S., Chan, W., Modugno, F., Notkin, D. & Reese, R. (1996), Model checking large software specifications, in ‘4th Symposium on the Foundations of Software Engineering’, ACM/SIGSOFT, pp. 156–166.
Bryant, R. (1986), ‘Graph-based algorithm for boolean function manipulation’, IEEE Transactions Computers C(35), 1035–1044.
Clarke, E. & Emerson, E. A. (1981), Design and synthesis of synchronization skeletons for branching time temporal logic, in ‘Logics of Programs: Workshop’, Vol. 131 of Lecture Notes in Computer Science, Springer Verlag, pp. 52–71.
Clarke, E., Emerson, E. & Sistla, A. (1986), ‘Automatic verification of finitestate concurrent systems using temporal logic specifications’, ACM Transactions On Programming Languages and Systems 8 (2), 244–263.
Iwashita, H., Nakata, T. & Hirose, F. (1996), CTL model checking based on forward state traversal, in ‘ICCAD’96’, p. 82.
Madre, J.-C. (1990), PRIAM Un outil de vérification formelle des circuits intégrés digitaux, PhD thesis, Ecole nationale supérieure des télécommunications, Paris, France. 90 E 007.
McMillan, K. (1993), Symbolic Model Checking, Kluwer Academic Publishers.
Queille, J.-P. & Sifakis, J. (1981), Specification and verification of concurrent systems in CESAR, in ‘Procs. 5th international symposium on programming’, Vol. 137 of Lecture Notes in Computer Science, Springer Verlag, pp. 244–263.
Tarski, A. (1955), ‘A lattice-theoretical fixpoint theorem and its applications’, Pacific J. Math pp. 285–309.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 IFIP
About this chapter
Cite this chapter
Déharbe, D., Moreira, A.M. (1997). Using induction and BDDs to model check invariants. In: Li, H.F., Probst, D.K. (eds) Advances in Hardware Design and Verification. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35190-2_13
Download citation
DOI: https://doi.org/10.1007/978-0-387-35190-2_13
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2885-8
Online ISBN: 978-0-387-35190-2
eBook Packages: Springer Book Archive