Data processing: software development – installation – and managem – Software program development tool – Testing or debugging
Reexamination Certificate
2005-08-04
2011-10-25
Zhen, Li (Department: 2197)
Data processing: software development, installation, and managem
Software program development tool
Testing or debugging
C714S033000, C717S135000
Reexamination Certificate
active
08046746
ABSTRACT:
Symbolic execution identifies possible execution paths of a computer program or method, each having certain constraints over the input values. The symbolic execution also records updates of memory locations, e.g. updates of the fields of symbolic objects in the heap of an object oriented program, involving a description of the previous heap, the updated symbolic object, a field identification, and a newly assigned symbolic value. The symbolic execution can also record calls to summarized methods, involving a description of previous calls, an identification of the summarized methods, and its symbolic arguments. The behavior of summarized methods can be expressed by axioms. Axioms describe the relationship between summarized methods under certain conditions. Axioms can be generated from parameterized unit tests. A parameterized unit test is a method with parameters which executes a sequence of calls to methods of an implementation under test; it asserts constraints over the inputs and outputs of the calls. A software testing program receives a parameterized unit test of an implementation under test, and symbolically executes the parameterized unit test. It can re-use axioms generated from other parameterized unit tests, and use them to emulate summarized methods.
REFERENCES:
patent: 5784553 (1998-07-01), Kolawa et al.
patent: 7089542 (2006-08-01), Brand et al.
patent: 7373636 (2008-05-01), Barry et al.
patent: 7389223 (2008-06-01), Atkin et al.
patent: 7496791 (2009-02-01), Tillmann et al.
patent: 7587636 (2009-09-01), Tillmann et al.
patent: 7797687 (2010-09-01), Tillmann et al.
patent: 2003/0097650 (2003-05-01), Bahrs et al.
patent: 2004/0117772 (2004-06-01), Brand et al.
patent: 2004/0243951 (2004-12-01), Hall
patent: 2005/0050391 (2005-03-01), Grieskamp et al.
patent: 2005/0120274 (2005-06-01), Haghighat et al.
patent: 2005/0204201 (2005-09-01), Meenakshisundaram et al.
patent: 2005/0223362 (2005-10-01), Whitlock et al.
patent: 2006/0085156 (2006-04-01), Kolawa et al.
patent: 2006/0253739 (2006-11-01), Godefroid et al.
patent: 2007/0033440 (2007-02-01), Tillmann et al.
Sidney L. Hantler and James C. King. “An Introduction to Proving the Correctness of Programs.” ACM Computing Surveys (CSUR) vol. 8 , Issue 3 (Sep. 1976) pp. 331-353.
Sarfraz Khurshid, Corina S Pãsãreanu, and Willem Visser. Generalized symbolic execution for model checking and testing. Proceedings of the 9th International Conference on Tools and Algorithms for Construction and Analysis of Systems (Lecture Notes in Computer Science, vol. 2619), Garavel H, Hatcliff J (eds.). Springer: Berlin, 2003; 553-568.
Robin M. Roos. Java data objects. Chapter 8, section 8.1. Pearson Education Ltd. 2003. Accessed from Safari Books on Feb. 12, 2009. (URL http://proquest.safaribooksonline.com/print?xmlid=0321123808/ch081ev1sec1).
Nikolai Tillmann, Wolfram Schulte, Wolfgang Grieskamp. “Parameterized Unit Tests.” Microsoft Research Technical Report. May 2005.
Nikolai Tillmann, Wolfram Schulte. “Parameterized Unit Tests.” ESEC/FSE'05. Sep. 5, 2005.
Jian Zhang, Chen Xu and Xiaoliang Wang. “Path-Oriented Test Data Generation Using Symbolic Execution and Constraint Solving Techniques.” Proceedings of the Software Engineering and Formal Methods, Second International Conference. Sep. 28, 2004. pp. 242-250.
Claessen, Koen, and John Hughes. “QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs.” 2000. Proceedings of the fifth ACM SIGPLAN international conference on Functional programming. pp. 268-279.
Cheatham, Jr., Thomas E.; Glenn H. Holloway; and Judy A. Townley. “Symbolic Evaluation and the Analysis of Programs.” Jul. 1979. IEEE Transactions on Software Engineering, vol. SE-5, No. 4. pp. 402-417.
Ambert et al., “BZ-TT: A Tool-Set for Test Generation from Z and B using Constraint Logic Programming,”Formal Approaches to Testing of Software, FATES 2002 workshop of CONCUR '02, INRIA Report, Aug. 2002, pp. 105-119.
Ball, “Formalizing Counterexample-driven Refinement with Weakest Preconditions,”Proceedings of 2004 Marktoberdorf Summer School, Dec. 10, 2004, 19 pages.
Barnett et al., “The Spec# Programming System: An Overview,” Construction and Analysis of Safe, Secure, and Interoperable Smart Devices: International Workshop,CASSIS 2004, vol. 3362 of LNCS, 2005, pp. 49-69.
Barnett et al., “99.44% pure: Useful Abstractions in Specifications,”Conference Proceedings ICIS report NIII-R0426, University of Nijmegen, 2004, pp. 11-19.
Bernot et al., “Software testing based on formal specifications: a theory and a tool,”Softw. Eng. J., 6(6)387-405, 1991.
Bidoit et al., “Algebraic system specification and development,”Springer-Verlag, Chapter 1, 1991, 12 pages.
Bierman et al., “MJ: An imperative core calculus for Java and Java with effects,”University of Cambridge Computer Laboratory, Technical Report 563, 2003, 53 pages.
Boyapati et al., “Korat: Automated Testing Based on Java Predicates, ”Proc. International Symposium on Software Testing and Analysis, 2002, pp. 123-133.
Brucker et al., “Symbolic Test Case Generation for Primitive Recursive Functions,”FATES, vol. 3395 ofLecture Notes in Computer Science, Springer, 2004, pp. 16-32.
Bush et al., “A static analyzer for finding dynamic programming errors,”Softw. Pract. Exper., 30(7):775-802, 2000.
Csallner et al., “Check 'n' Crash: Combining Static Checking and Testing,”27th International Conference on Software Engineering, May 2005, pp. 422-431.
Csallner et al., “JCrasher: an automatic robustness tester for Java,”Software—Practice&Experience 2004, Dec. 18, 2003, pp. 1025-1051.
Detlefs et al., “Simplify: A Theorem Prover for Program Checking,”Hewlett Packard Systems Research Center, 2003, 121 pages.
Dick et al., “Automating the Generation and Sequencing of Test Cases from Model-Based Specifications, ”Industrial Strength Formal Methods, Formal Methods Europe(FME'93),Proceedings, vol. 670 ofLNCS, Springer, 1993, pp. 268-284.
Doong et al., “The ASTOOT Approach to Testing Object-Oriented Programs,”ACM Trans. Softw. Eng. Methodol., 3(2):101-130, 1994.
Flanagan et al., “Extended Static Checking for Java,”Proc. the ACM SIGPLAN 2002 Conference on Programming language design and implementation, ACM Press, 2002, pp. 234-245.
Henkel et al., “Discovering Algebraic Specifications from Java Classes,”Proc. 17th European Conference on Object-Oriented Programming, 2003, pp. 431-456.
JCrasher documents, http://www.cc.gatech.edu/˜csallnch/jcrasher, 11 pages, downloaded Aug. 4, 2004.
Jalote, “Testing the Completeness of Specifications,”IEEE Trans. Softw. Eng., 15(5):526-531, 1989.
Jeffries et al., “Extreme Programming Installed,” Chapters 13, 14, and 29,Addison Wesley, Oct. 2000, 30 pages.
King, “Symbolic Execution and Program Testing,”Commun. ACM, 19(7):385-394, 1976.
Lahiri et al., “An Efficient Decision Procedure for UTVPI Constraints,”Technical Report MSR-TR-2005-67, Jun. 15, 2005, 18 pages.
Lahiri et al., “An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals,”Technical Report MSR-TR-2005-61, May 26, 2005, 16 pages.
Lahiri et al., Predicate Abstraction via Symbolic Decision Procedures,Technical Report MSR-TR-2005-53, May 26, 2005, 19 pages.
Leino et al., “A two-tier technique for supporting quantifiers in a lazily proof-explicating theorem prover,”TACAS 2005, Oct. 2004, 13 pages.
Loeckx et al., “The Foundations of Program Verification, 2nd Edition,” Chapter 6,Wiley, 1987, 23 pages.
Marinov et al., “TestEra: A Novel Framework for Automated Testing of Java Programs,”Proc. 16th IEEE International Conference on Automated Software Engineering, 2001, pp. 22-31.
Newkirk et al., “Test-Driven Development in Microsof
Grieskamp Wolfgang
Schulte Wolfram
Tillmann Nikolai
Klarquist & Sparkman, LLP
Kretzmer Erika
Microsoft Corporation
Zhen Li
LandOfFree
Symbolic execution of object oriented programs with... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Symbolic execution of object oriented programs with..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Symbolic execution of object oriented programs with... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-4302135