Yamini Kannan
ABSTRACT
Local data structure invariants are asserted over a bounded fragment of a data structure around a distinguished node M of the data structure. An example of such an invariant for a sorted doubly linked list is "for all nodes M of the list, if M ≠ null and M.next ≠ null, then M.next.prev = M and M.value ≤ M.next.value." It has been shown that such local invariants are both natural and sufficient for describing a large class of data structures. This paper explores a novel technique, called Krystal, to infer likely local data structure invariants using a variant of symbolic execution, called universal symbolic execution. Universal symbolic execution is like traditional symbolic execution except the fact that we create a fresh symbolic variable for every read of a lvalue that has no mapping in the symbolic state rather than creating a symbolic variable only for inputs. This helps universal symbolic execution to symbolically track data flow for all memory locations along an execution even if input values do not flow directly into those memory locations. We have implemented our algorithm and applied it to several data structure implementations in Java. Our experimental results show that we can infer many interesting local invariants for these data structures.
- R. Alur, P. Cerny, G. Gupta, P. Madhusudan, W. Nam, and A. Srivastava. Synthesis of Interface Specifications for Java Classes. In Proceedings of POPL'05 (32nd ACM Symposium on Principles of Programming Languages), 2005.]] Google Scholar
Digital Library
- G. Ammons, R. Bodik, and J. R. Larus. Mining specifications. SIGPLAN Not., 37(1):4--16, 2002.]] Google ScholarDigital Library
- L. Clarke. A system to generate test data and symbolically execute programs. IEEE Trans. Software Eng., 2:215--222, 1976.]] Google ScholarDigital Library
- P. D. Coward. Symbolic execution systems-a review. Software Engineering Journal, 3(6):229--239, 1988.]] Google ScholarDigital Library
- C. Csallner, N. Tillmann, and Y. Smaragdakis. DySy: Dynamic symbolic execution for invariant inference. In 30th ACM/IEEE International Conference on Software Engineering (ICSE), May 2008. To appear.]] Google ScholarDigital Library
- B. Dutertre and L. M. de Moura. A fast linear-arithmetic solver for dpll(t). In Computer Aided Verification, volume 4144 of LNCS, pages 81--94, 2006.]] Google ScholarDigital Library
- M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering, 27(2):99--123, Feb. 2001.]] Google ScholarDigital Library
- M. D. Ernst, A. Czeisler, W. G. Griswold, and D. Notkin. Quickly detecting relevant program invariants. In Proceedings of the 22nd International Conference on Software Engineering, pages 449--458, June 2000.]] Google ScholarDigital Library
- M. D. Ernst, W. G. Griswold, Y. Kataokay, and D. Notkin. Dynamically discovering program invariants involving collections. In TR UW-CSE-99-11-02, University of Washington, 2000.]]Google Scholar
- C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In Proc. of the ACM SIGPLAN Conference on Programming language design and implementation (PLDI'02), pages 234--245, 2002.]] Google ScholarDigital Library
- C. Flanagan and R. M. Leino. Houdini, an annotation assistant for esc/java. In Proceedings of the International Symposium of Formal Methods Europe (FME), pages 500--517, March 2001.]] Google ScholarDigital Library
- P. Godefroid, N. Klarlund, and K. Sen. DART: Directed automated random testing. In Proc. of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI), 2005.]] Google ScholarDigital Library
- S. Hangal and M. S. Lam. Tracking down software bugs using automatic anomaly detection. In Proceedings of the International Conference on Software Engineering, May 2002.]] Google ScholarDigital Library
- S. Khurshid, C. S. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Proc. 9th Int. Conf. on TACAS, pages 553--568, 2003.]] Google ScholarDigital Library
- J. C. King. Symbolic Execution and Program Testing. Communications of the ACM, 19(7):385--394, 1976.]] Google ScholarDigital Library
- G. Lee, J. Morris, K. Parker, G. A. Bundell, and P. Lam. Using symbolic execution to guide test generation: Research articles. Softw. Test. Verif. Reliab., 15(1):41--61, 2005.]] Google ScholarDigital Library
- F. Logozzo. Automatic inference of class invariants. In Proceedings of the 5th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI '04), January 2004.]]Google ScholarCross Ref
- M. Z. Malik, A. Pervaiz, , and S. Khurshid. Generating representation invariants of structurally complex data. In TACAS, pages 34--49, 2007.]] Google ScholarDigital Library
- S. McPeak and G. C. Necula. Data structure specifications via local equality axioms. In Proceedings of Computer Aided Verification (CAV), pages 476--490, 2005.]] Google ScholarDigital Library
- J. Mitchell. Foundations for Programming Languages. MIT Press, 1996.]] Google ScholarDigital Library
- K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. Technical Report UIUCDCS-R-2005-2597, UIUC, 2005.]]Google ScholarCross Ref
- K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. In 5th joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE'05). ACM, 2005.]] Google ScholarDigital Library
- M. Taghdiri and D. Jackson. Inferring specifications to detect errors in code. Automated Software Engg., 14(1):87--121, 2007.]] Google ScholarDigital Library
- N. Tillmann, F. Chen, and W. Schulte. Discovering likely method specifications. In ICFEM, pages 717--736, 2006.]] Google ScholarDigital Library
- R. Vallee-Rai, L. Hendren, V. Sundaresan, P. Lam, E. Gagnon, and P. Co. Soot -- a Java optimization framework. In CASCON 1999, pages 125--135, 1999.]] Google ScholarDigital Library
- W. Visser, C. S. Pasareanu, and S. Khurshid. Test input generation with Java PathFinder. In Proc. 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 97--107, 2004.]] Google ScholarDigital Library
- S. Visvanathan and N. Gupta. Generating test data for functions with pointer inputs. In 17th IEEE International Conference on Automated Software Engineering, 2002.]] Google ScholarDigital Library
- J. Whaley, M. C. Martin, and M. S. Lam. Automatic Extraction of Object-Oriented Component Interfaces. In Proceedings of ACM SIGSOFT ISSTA'02 (International Symposium on Software Testing and Analysis), 2002.]] Google ScholarDigital Library
- T. Xie, D. Marinov, W. Schulte, and D. Notkin. Symstra: A framework for generating object-oriented unit tests using symbolic execution. In Procs. of TACAS, 2005.]] Google ScholarDigital Library
- J. Yang and D. Evans. Dynamically inferring temporal properties. In PASTE '04, pages 23--28. ACM, 2004.]] Google ScholarDigital Library
Index Terms
- Universal symbolic execution and its application to likely data structure invariant generation
Recommendations
Dynamically Discovering Likely Program Invariants to Support Program Evolution
Special issue on 1999 international conference on software engineeringExplicitly stated program invariants can help programmers by identifying program properties that must be preserved when modifying code. In practice, however, these invariants are usually implicit. An alternative to expecting programmers to fully ...
Towards systematic, comprehensive trace generation for behavioral pattern detection through symbolic execution
PASTE '11: Proceedings of the 10th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software toolsIn reverse engineering, dynamic pattern detection is accomplished by collecting execution traces and comparing them to expected behavioral patterns. The traces are collected by manually executing the program under study and therefore represent only part ...
Parallel symbolic execution for structural test generation
ISSTA '10: Proceedings of the 19th international symposium on Software testing and analysisSymbolic execution is a popular technique for automatically generating test cases achieving high structural coverage. Symbolic execution suffers from scalability issues since the number of symbolic paths that need to be explored is very large (or even ...
Comments