Abstract
Generating likely invariants using dynamic analyses is becoming an increasingly effective technique in software checking methodologies. This paper presents Deryaft, a novel algorithm for generating likely representation invariants of structurally complex data. Given a small set of concrete structures, Deryaft analyzes their key characteristics to formulate local and global properties that the structures exhibit. For effective formulation of structural invariants, Deryaft focuses on graph properties, including reachability, and views the program heap as an edge-labeled graph.
Deryaft outputs a Java predicate that represents the invariants; the predicate takes an input structure and returns true if and only if it satisfies the invariants. The invariants generated by Deryaft directly enable automation of various existing frameworks, such as the Korat test generation framework and the Juzi data structure repair framework, which otherwise require the user to provide the invariants. Experimental results with the Deryaft prototype show that it feasibly generates invariants for a range of subject structures, including libraries as well as a stand-alone application.
Chapter PDF
Similar content being viewed by others
Keywords
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
Adjie-Winoto, W., et al.: The design and implementation of an intentional naming system. In: Proc. 17th ACM Symposium on Operating Systems Principles (SOSP), Kiawah Island (December 1999)
Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis by predicate abstraction. In: Proc. 6th International Conference on Verification, Model Checking and Abstract Interpretation, Paris, France (2005)
Beck, K., Gamma, E.: Test infected: Programmers love writing tests. Java Report 3(7) (1998)
Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on Java predicates. In: Proc. International Symposium on Software Testing and Analysis (ISSTA) (July 2002)
Cormen, T.H., Leiserson, C.E.: Introduction to Algorithms. The MIT Press, Cambridge (1990)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. 5th Annual ACM Symposium on the Principles of Programming Languages (POPL), Tucson, Arizona (1978)
Ernst, M.D.: Dynamically Discovering Likely Program Invariants. PhD thesis, University of Washington Department of Computer Science and Engineering (August 2000)
Flanagan, C., et al.: Extended static checking for Java. In: Proc. ACM SIGPLAN 2002 Conference on Programming language design and implementation (2002)
German, S.M., Wegbreit, B.: A synthesizer of inductive assertions. IEEE Trans. Software Eng. 1(1) (1975)
Ghiya, R., Hendren, L.J.: Is it a tree, a DAG, or a cyclic graph? A shape analysis for heap-directed pointers in C. In: POPL ’96: Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (1996)
Gupta, N., Heidepriem, Z.V.: A new structural coverage criterion for dynamic detection of program invariants. In: Proc. 18th Conference on Automated Software Engineering (ASE), San Diego, CA (October 2003)
Hangal, S., Lam, M.S.: Tracking down software bugs using automatic anomaly detection. In: ICSE ’02: Proceedings of the 24th International Conference on Software Engineering (2002)
Jackson, D.: Software Abstractions: Logic, Language and Analysis. The MIT Press, Cambridge (2006)
Jackson, D., Fekete, A.: Lightweight analysis of object interactions. In: Proc. Fourth International Symposium on Theoretical Aspects of Computer Software, Sendai, Japan (October 2001)
Khurshid, S., García, I., Suen, Y.L.: Repairing structurally complex data. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, Springer, Heidelberg (2005)
Khurshid, S., Malik, M.Z., Uzuncaova, E.: An automated approach for writing Alloy specifications using instances. In: 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, Paphos, Cyprus (2006)
Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report TR 98-06i, Department of Computer Science, Iowa State University (June 1998)
Marinov, D., et al.: Optimizations for compiling declarative models into boolean formulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, Springer, Heidelberg (2005)
Moeller, A., Schwartzbach, M.I.:The pointer assertion logic engine. In: Proc. SIGPLAN Conference on Programming Languages Design and Implementation, Snowbird, UT (June 2001)
Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems (TOPLAS) (January 1998)
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using groebner bases. In: POPL ’04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages (2004)
Taghdiri, M.: Inferring specifications to detect errors in code. In: Proceedings of the 19th IEEE International Conference on Automated Software Engineering, Washington, DC (2004)
Tiwari, A., et al.: A technique for invariant generation. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, Springer, Heidelberg (2001)
Vaziri, M., Holzmann, G.: Automatic detection of invariants in spin. In: Proc. SPIN Workshop on Software Model Checking (November 1998)
Whaley, J., Martin, M.C., Lam, M.S.: Automatic extraction of object-oriented component interfaces. In: Proc. International Symposium on Software Testing and Analysis, ISSTA (July 2002)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Malik, M.Z., Pervaiz, A., Khurshid, S. (2007). Generating Representation Invariants of Structurally Complex Data. In: Grumberg, O., Huth, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2007. Lecture Notes in Computer Science, vol 4424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71209-1_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71208-4
Online ISBN: 978-3-540-71209-1
eBook Packages: Computer ScienceComputer Science (R0)