Abstract
We present a framework for verifying that programs correctly preserve important data structure consistency properties. Results from our implemented system indicate that our system can effectively enable the scalable verification of very precise data structure consistency properties within complete programs. Our system treats both internal properties, which deal with a single data structure implementation, and external properties, which deal with properties that involve multiple data structures. A key aspect of our system is that it enables multiple analysis and verification packages to productively interoperate to analyze a single program. In particular, it supports the targeted use of very precise, unscalable analyses in the context of a larger analysis and verification system. The integration of different analyses in our system is based on a common set-based specification language: precise analyses verify that data structures conform to set specifications, whereas scalable analyses verify relationships between data structures and preconditions of data structure operations.
There are several reasons why our system may be of interest in a broader program analysis and verification effort. First, it can ensure that the program satisfies important data structure consistency properties, which is an important goal in and of itself. Second, it can provide information that insulates other analysis and verification tools from having to deal directly with pointers and data structure implementations, thereby enabling these tools to focus on the key properties that they are designed to analyze. Finally, we expect other developers to be able to leverage its basic structuring concepts to enable the scalable verification of other program safety and correctness properties.
Chapter PDF
Similar content being viewed by others
Keywords
- Data Structure
- Mathematical Abstraction
- Interactive Theorem Prove
- Tractable Fragment
- Procedure Precondition
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proc. ACM PLDI (2001)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: CASSIS: Int. Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart devices (2004)
Blume, W., Eigenmann, R.: Performance analysis of parallelizing compilers on the Perfect Benchmarks programs. IEEE Transactions on Parallel and Distributed Systems 3(6), 643–656 (1992)
Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Springer, Heidelberg (1997)
Chase, D.R., Wegman, M., Zadeck, F.K.: Analysis of pointers and structures. In: Proc. ACM PLDI (1990)
Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: Proc. ACM PLDI (2002)
Jones, C.B.: Systematic Software Development using VDM. Prentice Hall International, UK (1986)
Kuncak, V., Lam, P., Rinard, M.: Role analysis. In: Annual ACM Symp. on Principles of Programming Languages (POPL) (2002)
Kuncak, V., Rinard, M.: Decision procedures for set-valued fields. In: 1st International Workshop on Abstract Interpretation of Object-Oriented Languages (AIOOL 2005) (2005)
Lam, P., Kuncak, V., Rinard, M.: On our experience with modular pluggable analyses. Technical Report 965, MIT CSAIL (September, 2004)
Lam, P., Kuncak, V., Rinard, M.: Cross-cutting techniques in program specification and analysis. In: 4th International Conference on Aspect-Oriented Software Development (AOSD 2005) (2005)
Lam, P., Kuncak, V., Rinard, M.: Generalized typestate checking for data structure consistency. In: 6th International Conference on Verification, Model Checking and Abstract Interpretation (2005)
Lam, P., Kuncak, V., Rinard, M.: Hob: A tool for verifying data structure consistency. In: 14th International Conference on Compiler Construction (tool demo) (April, 2005)
Lev-Ami, T., Reps, T., Sagiv, M., Wilhelm, R.: Putting static analysis to work for verification: A case study. In: International Symposium on Software Testing and Analysis (2000)
Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Proc. 7th International Static Analysis Symposium (2000)
Marinov, D.: Credible compilation. Master’s thesis, Massachusetts Institute of Technology (2000)
Marnette, B., Kuncak, V., Rinard, M.: On algorithms and complexity for sets with cardinality constraints. Technical report, MIT CSAIL (August, 2005)
O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, Springer, Heidelberg (2001)
Ramalingam, G., Warshavsky, A., Field, J., Goyal, D., Sagiv, M.: Deriving specialized program analyses for certifying component-client conformance. In: PLDI (2002)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th LICS, pp. 55–74 (2002)
Rinard, M., Marinov, D.: Credible compilation with pointers. In: Proceedings of the Workshop on Run-Time Result Verification (1999)
Rinetzky, N.: Interprocedural shape analysis. Master’s thesis, Technion - Israel Institute of Technology (2000)
Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM TOPLAS 20(1), 1–50 (1998)
Steensgaard, B.: Points-to analysis in almost linear time. In: Proc. 23rd ACM POPL, Petersburg Beach, FL (January, 1996)
Sălcianu, A.D., Rinard, M.: Purity and side-effect analysis for java programs. In: Proc. 6th International Conference on Verification, Model Checking and Abstract Interpretation (to appear, January 2005)
Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. In: POPL 2005 (2005)
Yang, J., Twohey, P., Engler, D., Musuvathi, M.: Using model checking to find serious file system errors. In: OSDI 2004 (2004)
Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 530–545. Springer, Heidelberg (2004)
Yorsh, G., Skidanov, A., Reps, T., Sagiv, M.: Automatic assume/guarantee reasoning for heap-manupilating programs. In: 1st AIOOL Workshop (2005)
Zee, K., Lam, P., Kuncak, V., Rinard, M.: Combining theorem proving with static analysis for data structure consistency. In: International Workshop on Software Verification and Validation (SVV 2004), Seattle (November, 2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Kuncak, V., Lam, P., Zee, K., Rinard, M. (2008). Implications of a Data Structure Consistency Checking System. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)