Abstract
State explosion in model checking continues to be the primary obstacle to widespread use of software model checking. The large input ranges of variables used in software is the main cause of state explosion. As software grows in size and complexity, the problem only becomes worse. As such, model checking research into data abstraction as a way of mitigating state explosion has become more and more important. Data abstractions aim to reduce the effect of large input ranges. This work focuses on a static program analysis technique called dead variable analysis. The goal of dead variable analysis is to discover variable assignments that are not used. When applied to model checking, this allows us to ignore the entire input range of dead variables and thus reduce the size of the explored state space.
Prior research into dead variable analysis for model checking does not make full use of dynamic run-time information that is present during model checking. We present an algorithm for intraprocedural dead variable analysis that uses dynamic run-time information to find more dead variables on-the-fly and further reduce the size of the explored state space. We introduce a definition for the maximal state space reduction possible through an on-the-fly dead variable analysis and then show that our algorithm produces a maximal reduction in the absence of non-determinism.
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
Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: principles, techniques, and tools. Addison-Wesley Longman Publishing Co., Inc., Boston (1986)
Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for Boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN Model Checking and Software Verification. LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000)
Bozga, M., Fernandez, J., Ghirvu, L.: State space reduction based on live variables analysis. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 164–178. Springer, Heidelberg (1999)
Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. on Programming Languages and Systems 16(5), 1512–1542 (1994)
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Păsăreanu, C.S., Zheng, R., Zheng, H.: Bandera: extracting finite-state models from Java source code. In: International Conference on Software Engineering, pp. 439–448 (2000)
Dong, Y., Ramakrishnan, C.R.: An optimizing compiler for efficient model checking. In: FORTE XII / PSTV XIX 1999: Proceedings of the IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XII) and Protocol Specification, Testing and Verification (PSTV XIX), pp. 241–256. Kluwer, B.V., Dordrecht (1999)
The Gnu project debugger (2006), available at http://sources.redhat.com/gdb/
GNU libraries for 68hc11 and 68hc12 (2005), available at http://gel.sourceforge.net/
Havelund, K., Pressburger, T.: Model checking Java programs using Java pathfinder (1998)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with Blast. In: Ball, T., Rajamani, S.K. (eds.) Model Checking Software. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)
Holzmann, G.J.: The engineering of a model checker: the Gnu i-protocol case study revisited. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) Theoretical and Practical Aspects of SPIN Model Checking. LNCS, vol. 1680, Springer, Heidelberg (1999)
Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)
Lewis, M.S., Jones, M.D.: A dead variable analysis for explicit model checking. In: ACM SIGPLAN 2006 Workshop on Partial Evaluation and Program (2006)
Mercer, E.G., Jones, M.: Model checking machine code with the GNU debugger. In: Godefroid, P. (ed.) Model Checking Software. LNCS, vol. 3639, pp. 251–265. Springer, Heidelberg (2005)
Pelánek, R.: On-the-fly state space reductions. Technical Report FIMU-RS-2005-2003, Faculty of Informatics Masaryk University Brno (2005)
Robby, M., Dwyer, J.: Bogor: an extensible and highly-modular software model checking framework (2003)
Yorav, K., Grumberg, O.: Static analysis for state-space reductions preserving temporal logics. Form. Methods Syst. Des. 25(1), 67–96 (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Self, J.P., Mercer, E.G. (2007). On-the-Fly Dynamic Dead Variable Analysis. In: Bošnački, D., Edelkamp, S. (eds) Model Checking Software. SPIN 2007. Lecture Notes in Computer Science, vol 4595. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73370-6_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-73370-6_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73369-0
Online ISBN: 978-3-540-73370-6
eBook Packages: Computer ScienceComputer Science (R0)