Although BMC can find bugs in larger designs than BDD-based methods, the correctness of a property is guaranteed only for the analysis bound. However, one can augment BMC for performing proofs by induction [66, 67]. A completeness bound has been proposed [66, 67], to provide an inductive proof of correctness for safety properties based on the longest loop-free path between states.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Rights and permissions
Copyright information
© 2007 Springer Science+Business Media, LLC
About this chapter
Cite this chapter
(2007). Proof by Induction. In: SAT-Based Scalable Formal Verification Solutions. Series on Integrated Circuits and Systems. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-69167-1_9
Download citation
DOI: https://doi.org/10.1007/978-0-387-69167-1_9
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-69166-4
Online ISBN: 978-0-387-69167-1
eBook Packages: Computer ScienceComputer Science (R0)