Abstract
Automated abstraction refinement methods have shown significant promise in analyzing low-level software, such as operating system device drivers, and other control-oriented codes. For example, the SLAM toolkit from Microsoft research [1] has proved effective in finding control errors (such as illegal use of kernel API functions) in real-world device driver codes. SLAM is based on predicate abstraction, using a counterexample-based abstraction refinement heuristic. This gives it the ability to focus the abstraction on state predicates that are relevant to the proof (or falsification) of a given property. This ability allows SLAM and similar tools to scale to real codes of moderate size, albeit only in the case when the property is fairly shallow, in the sense that it requires only a small amount of information about the program’s state to prove it.
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
References
Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL, pp. 1–3 (2002)
Chou, A., Yang, J., Chelf, B., Hallem, S., Engler, D.R.: An empirical study of operating system errors. In: Symposium on Operating Systems Principles, pp. 73–88 (2001)
Distefano, D., O’Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 287–302. Springer, Heidelberg (2006)
Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Neil, D., Jones, N.D., Leroy, X. (eds.) POPL, pp. 232–244. ACM Press, New York (2004)
McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1), 101–121 (2005)
Nanevski, A., Magill, S., Clarke, E., Lee, P.: Inferring invariants in separation logic for imperative list-processing programs. In: Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE) (2006)
Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: POPL, pp. 105–118 (1999)
Sullivan, M., Chillarege, R.: Software defects and their impact on system availability - a study of field failures in operating systems. In: 21st Int. Symp. on Fault-Tolerant Computing (FTCS-21), pp. 2–9 (1991)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
McMillan, K.L. (2007). Toward Property-Driven Abstraction for Heap Manipulating Programs. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds) Automated Technology for Verification and Analysis. ATVA 2007. Lecture Notes in Computer Science, vol 4762. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75596-8_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-75596-8_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75595-1
Online ISBN: 978-3-540-75596-8
eBook Packages: Computer ScienceComputer Science (R0)