Abstract
SAT based Bounded Model Checking (BMC) is an efficient method for detecting logical errors in finite-state transition systems. Given a transition system, an LTL property, and a user defined bound k, a bounded model checker generates a propositional formula that is satisfiable if and only if a counterexample to the property of length up to k exists. Standard SAT checkers can be used to check this formula.BMCis complete if k is larger than some pre-computed threshold. It is still unknown how to compute this threshold for general properties.We show that the longest initialized loop-free path in the state graph, also known as the recurrence diameter, is sufficient for Fp properties. The recurrence diameter is also a known over-approximation for the threshold of simple safety properties (Gp).We discuss various techniques to compute the recurrence diameter efficiently and provide experimental results that demonstrate the benefits of using the new approach.
This research was sponsored by the Semiconductor Research Corporation (SRC) under contract no. 99-TJ-684, the National Science Foundation (NSF) under grant no. CCR-9803774, the Office of Naval Research (ONR), and the Naval Research Laboratory (NRL) under contract no. N00014-01-1-0796. The views and conclusions contained in this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of SRC, NSF, ONR, NRL, the U.S. government or any other entity.
In all previous publications on this matter, the term ‘diameter’ was used to denote what we refer to as the completeness threshold. Since the term diameter has a specific meaning in graph theory that coincides with the completeness threshold only for some properties (as we explain later), it is unsuitable for describing the general case.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for Construction and Analysis of Systems, pages 193–207, 1999.
E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, Cambridge, MA, 1999.
A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Design Automation Conference (DAC’99), 1999.
A. Biere, C. Artho, and V. Schuppan. Liveness checking as safety checking. In FMICS workshop 2002, 2002.
J. Baumgartner, A. Kuehlmann, and J. Abraham. Property checking via structural analysis. In Proc. 14th Intl. Conference on Computer Aided Verification (CAV’02), 2002.
M. Mneimneh and K. Sakallah. SAT-based sequential depth computation. In Constraints in formal verification workshop, Cornell University, Ithaca, NewYork, Sep 2002.
A. Biere, E. Clarke, R. Raimi, and Y. Zhu. Verifying safety properties of a PowerPCTM microprocessor using symbolic model checking without bdds. In N. Halbwachs and D. Peled, editors, Proc. 11th Intl. Conference on Computer Aided Verification (CAV’99), LNCS. Springer-Verlag, 1999.
D.E. Knuth. The Art of Computer Programming, volume 3: Sorting and Searching. Addison Wesley, 1973.
M. Ajtai, J. Komlós, and S. Szemerédi. An O(N logN) sorting network. In Proceedings of the 25th ACM Symposium on Theory of Computing, pages 1–9, 1983.
K.E. Batcher. Sorting networks and their applications. In Proc. AFIPS Spring Joint Comput. Conf., volume 32, pages 307–314, 1968.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kroening, D., Strichman, O. (2003). Efficient Computation of Recurrence Diameters. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2003. Lecture Notes in Computer Science, vol 2575. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36384-X_24
Download citation
DOI: https://doi.org/10.1007/3-540-36384-X_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00348-9
Online ISBN: 978-3-540-36384-2
eBook Packages: Springer Book Archive