Abstract
Most approaches for model checking software are based on the generation of abstract models from source code, which may greatly reduce the search space, but may also introduce errors that are not present in the actual program.
In this paper, we propose a new model checker for the verification of native c++-programs. To allow platform independent model checking of the object code for concurrent programs, we have extended an existing virtual machine for c++ to include multi-threading and different exploration algorithms on a dynamic state description.
The error reporting capabilities and the lengths of counter-examples are improved by using heuristic estimator functions and state space compaction techniques that additionally reduce the exploration efforts.
The evaluation of four scalable simple example problems shows that our system StEAM can successfully enhance the detection of deadlocks and assertion violations.
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.
References
Ball, T., Rajamani, S.K.: The Slam Project: Debugging System Software via Static Analysis. In: ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 1–3 (2002)
Bosnacki, D., Dams, D., Holenderski, L.: A Heuristic for Symmetry Reductions with Scalarsets. In: International Symposium on FME: Formal Methods for Increasing Software Productivity, pp. 518–533 (2001)
Cattel, T.: Modeling and Verification of sC++ Applications. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 232–248. Springer, Heidelberg (1998)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)
Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Robby, Laubachand, S., Zheng, H.: Extracting Finite-state Models from Java Source Code. In: International Conference on Software Engineering (ICSE), pp. 439–448 (2000)
Demartini, C., Iosif, R., Sisto, R.: dSPIN: A dynamic extension of SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 261–276. Springer, Heidelberg (1999)
Dwyer, M., Hatcliff, J., Prasad, V., Robby: Exploiting Object Escape and Locking Information in Partial Order Reduction for Concurrent Object-Oriented Programs. To appear in Formal Methods in System Design Journal, FMSD (2004)
Edelkamp, S., Lafuente, A.L., Leue, S.: Trail-directed Model Checking. In: Stoller, S.D., Visser, W. (eds.) Electronic Notes in Theoretical Computer Science, vol. 55, Elsevier Science Publishers, Amsterdam (2001)
Edelkamp, S., Leven, P.: Directed Automated Theorem Proving. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol. 2514, pp. 145–159. Springer, Heidelberg (2002)
Edelkamp, S., Mehler, T.: Byte Code Distance Heuristics and Trail Direction for Model Checking Java Programs. In: 2nd Workshop on Model Checking and Artificial Intelligence (MoChArt), pp. 69–76 (2003)
Godefroid, P.: Model Checking for Programming Languages using Verisoft. In: Symposium on Principles of Programming Languages, pp. 174–186 (1997)
Groce, A., Visser, W.: Model Checking Java Programs using Structural Heuristics. In: International Symposium on Software Testing and Analysis (ISSTA), pp. 12–21 (2002)
Hatcliff, J., Tkachuck, O.: The Bandera Tools for Model-checking Java Source Code: A User’s Manual. Technical report, Kansas State University (1999)
Henzinger, A., Jhala, R., Majumdar, R., Sutre, G.: Software Verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)
Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)
Holzmann, G.J.: State Compression in SPIN. In: Third Spin Workshop, Twente University, The Netherlands (1997)
Holzmann, G.J.: The Model Checker SPIN. Software Engineering 23(5), 279–295 (1997)
Holzmann, G.J.: Logic Verification of ANSI-C code with SPIN. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 131–147. Springer, Heidelberg (2000)
Iosif, R.: Exploiting Heap Symmetries in Explicit-State Model Checking of Software. In: International Conference on Automated Software Engineering (ICSE), pp. 26–29 (2001)
Lluch-Lafuente, A., Leue, S., Edelkamp, S.: Partial Order Reduction in Directed Model Checking. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 112–127. Springer, Heidelberg (2002)
Mehler, T., Leven, P.: Introduction to StEAM - An Assembly-Level Software Model Checker. Technical report, University of Freiburg (2003)
Musuvathi, M., Park, D., Chou, A., Engler, D., Dill, D.: CMC: A Pragmatic Approach to Model Checking Real Code. In: Symposium on Operating Systems Design and Implementation, OSDI (2002)
Robby, M., Dwyer, B., Hatcliff, J.: Bogor: An Extensible and Highly-Modular Software Model Checking Framework. In: European Software Engineering Conference (ESEC), pp. 267–276 (2003)
Visser, W., Havelund, K., Brat, G., Park, S.: Java PathFinder - second generation of a Java model checker. In: Post-CAV Workshop on Advances in Verification, WAVe (2000)
Visser, W., Havelund, K., Brat, G., Park, S.: Model Checking Programs. In: International Conference on Automated Software Engineering (ICSE), pp. 3–12 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leven, P., Mehler, T., Edelkamp, S. (2004). Directed Error Detection in C++ with the Assembly-Level Model Checker StEAM. In: Graf, S., Mounier, L. (eds) Model Checking Software. SPIN 2004. Lecture Notes in Computer Science, vol 2989. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24732-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-24732-6_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21314-7
Online ISBN: 978-3-540-24732-6
eBook Packages: Springer Book Archive