Abstract
Current research in software model checking explores new techniques to handle the storage of visited states (usually called the heap). One approach consists in saving only parts or representations of the states in the heap. This paper presents a new technique to implement sound abstract matching of states. This kind of matching produces a reduction in the number of states and traces explored. With the aim of obtaining a useful result, it is necessary to establish some correctness conditions on the matching scheme. In this paper, we use static analysis to automatically construct an abstract matching function which depends on the program and the property to be verified. The soundness of the static analysis guarantees the soundness of verification. This paper describes the overall technique applied to Spin, the correctness issues and some examples which show its efficiency.
This work has been supported by the Spanish MEC under grant TIN2004-7943-C04.
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.
Similar content being viewed by others
References
Bosnacki, D.: Enhancing State Space Reduction Techniques for Model Checking. PhD thesis, Eindhoven Univ. of Technology (2001)
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Zheng, H.: Bandera: Extracting Finite-state Models from Java Source Code. In: Proc. of the 22nd Int. conference on Software engineering, pp. 439–448. ACM Press, New York (2000)
de la Cámara, P., Gallardo, M.M., Merino, P., Sanán, D.: Model Checking Software with Well-Defined APIs: the Socket Case. In: FMICS 2005: Proc. of the 10th int. workshop on Formal methods for industrial critical systems, pp. 17–26. ACM Press, New York (2005)
Clarke, E.M., Grumberg, H., Peled, D.: Model Checking (2000)
Gallardo, M.M., Merino, P., Pimentel, E.: A Generalized Semantics of Promela for Abstract Model Checking. Formal Aspects of Computing 16, 166–193 (2004)
Havelund, K., Pressburger, T.: Model Checking Java Programs using Java Pathfinder. International Journal of Software Tools for Technology Transfer 2(4), 366–381 (2000)
Holzmann, G.J., Joshi, R.: Model-Driven Software Verification. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 76–91. Springer, Heidelberg (2004)
Holzmann, G.J., Smith, M.H.: Software Model Checking: Extracting Verification Models from Source Code. Software Testing, Verification & Reliability 11(2), 65–79 (2001)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis (1998)
Pasareanu, C.S., Pelánek, R., Visser, W.: Concrete Model Checking with Abstract Matching and Refinement. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 52–66. Springer, Heidelberg (2005)
Peled, D., Valmari, A., Kokkarinen, I.: Relaxed Visibility Enhances Partial Order Reduction. Formal Methods in System Design 19(3), 275–289 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de la Cámara, P., del Mar Gallardo, M., Merino, P. (2006). Abstract Matching for Software Model Checking. In: Valmari, A. (eds) Model Checking Software. SPIN 2006. Lecture Notes in Computer Science, vol 3925. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691617_11
Download citation
DOI: https://doi.org/10.1007/11691617_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33102-5
Online ISBN: 978-3-540-33103-2
eBook Packages: Computer ScienceComputer Science (R0)