Abstract
Lazy abstraction builds up an abstract reachability tree by locally refining abstractions in order to eliminate spurious counterexamples in smaller and smaller subtrees. The method has proven useful to verify systems code. It is still open how good the method is as a decision procedure, i.e., whether the method terminates for already known decidable verification problems. In this paper, we answer the question positively for broadcast protocols and other infinite-state models in the class of so-called well-structured systems. This extends an existing result on systems with a finite bisimulation quotient.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Henzinger, T.A., et al.: Lazy abstraction. In: POPL, pp. 58–70 (2002)
Clarke, E.M., et al.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Henzinger, T.A., et al.: Software Verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)
Henzinger, T.A., et al.: Temporal-Safety Proofs for Systems Code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, Springer, Heidelberg (2002)
Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1-2), 63–92 (2001)
Ganty, P., Raskin, J.F., Van Begin, L.: A complete abstract interpretation framework for coverability properties of wsts. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 49–64. Springer, Heidelberg (2005)
Geeraerts, G., Raskin, J.F., Begin, L.V.: Expand, Enlarge, and Check: New algorithms for the coverability problem of wsts. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 287–298. Springer, Heidelberg (2004)
Raskin, J.-F., Van Begin, L., Geeraerts, G.: Expand, enlarge and check. made efficient. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 394–404. Springer, Heidelberg (2005)
Delzanno, G., Esparza, J., Podelski, A.: Constraint-Based Analysis of Broadcast Protocols. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 50–66. Springer, Heidelberg (1999)
Abdulla, P.A., et al.: General decidability theorems for infinite-state systems. In: LICS, pp. 313–321 (1996)
Bouajjani, A., et al.: Minimal state graph generation. Sci. Comput. Program. 18(3), 247–269 (1992)
Ball, T., Podelski, A., Rajamani, S.K.: Relative Completeness of Abstraction Refinement for Software Model Checking. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol. 2280, Springer, Heidelberg (2002)
McMillan, K.L.: Lazy Abstraction with Interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006)
Dickson, L.: Finiteness of the odd perfect and primitive abundant numbers with n prime factors. Amer. J. Math. 35, 413–422 (1913)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dimitrova, R., Podelski, A. (2008). Is Lazy Abstraction a Decision Procedure for Broadcast Protocols?. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2008. Lecture Notes in Computer Science, vol 4905. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78163-9_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-78163-9_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78162-2
Online ISBN: 978-3-540-78163-9
eBook Packages: Computer ScienceComputer Science (R0)