Data processing: software development – installation – and managem – Software program development tool – Testing or debugging
Reexamination Certificate
2006-04-04
2006-04-04
Dam, Tuan (Department: 2192)
Data processing: software development, installation, and managem
Software program development tool
Testing or debugging
C714S038110
Reexamination Certificate
active
07024661
ABSTRACT:
In a system for statically analyzing a specified computer, a verification condition generator converts the program into a logical equation, called a verification condition, and inserts program flow control labels into the sub-equations of the verification condition. The flow control labels identify conditional branch points in the specified computer program. A theorem prover is applied to the logical equation to determine truth of the logical equation, and when the truth of the logical equation cannot be proved, the theorem prover generates at least one counter-example identifying one of the conditions, one or more variable values inconsistent with that condition, and any of the flow control labels for conditional branch points of the program associated with the identified variable values. A post processing module converts each counter-example into an error message that includes a program trace when the counter-example identifies one or more of the flow control labels.
REFERENCES:
patent: 4920538 (1990-04-01), Chan et al.
patent: 5694539 (1997-12-01), Haley et al.
patent: 5854924 (1998-12-01), Rickel et al.
patent: 5909580 (1999-06-01), Crelier et al.
patent: 5987252 (1999-11-01), Leino et al.
patent: 6029002 (2000-02-01), Afifi et al.
patent: 6128774 (2000-10-01), Necula et al.
patent: 6374368 (2002-04-01), Mitchell et al.
patent: 6560774 (2003-05-01), Gordon et al.
“A Generalization of Dijkstra's Calculus”; Greg Nelson; Digital Systems Research Center; Apr. 2, 1987; #16; 57 pages.
“Ecstatic: An object-oriented programming language with an axiomatic semantics”; K. Rustan M. Leino; Digital Equipment Corporation Systems Research Center; Dec. 16, 1996; KRML 65-0; 42 pages.
“Extended Static Checking”; David L. Detlefs et al.; Compaq Systems Research Center; Dec. 18, 1998, #159; 44 pages.
“Checking Java programs via guarded commands”; Compaq Systems Research Center; May 21, 1999; SRC Technical Note 1999-002 ; 6 pages.
Detlefs, David L. “An Overview Of The Extended Static Checking System” Digital Equipment Corporation, Systems Research Center, 130 Lytton Ave, Palo Alto CA 94301, (Nov. 28, 1995), pp 1-9.
Intrinsa Corp. “A Technical Introduction To PREfix/Enterprise” (1998) pp 1-18.
Janssen et al. “Model Checking For Managers” Proceedings of the 6thInternational SPIN Workshop On Practical Aspects Of Model Checking, Toulouse, France, (Sep. 1999), pp 1-16.
Manasse et al. . “Correct Compilation Of Control Structures” AT&T Bell Laboratories, Murral Hill, New Jersey 07974, (Apr. 13, 1985), pp 1-20.
Millstein, Todd “Toward More Informative ESC/JAVA Warning Messages” http://gatekeeper.research.compaq.com/pu...1 -notes/src-1999-003-html/millstein.html, pp 1-2. Last Accessed on Nov. 21, 2001.
Rustan et al. “ESC/Java User's Manual” SRC Technical Note 2000-002, (Oct. 12, 2000), pp 1-92.
Leino, K. R. M. and Nelson, C. G., “An extended static checker for Modula-3”, in Kai Koskimies, Ed.,Compiler Construction: 7th International Conference, Apr. 1998 (CC'98),Lecture Notes in Computer Science, vol. 1383, pp. 302-305, (Springer-Verlag 1998).
Savage et al. “Eraser: A Dynamic Data Race Detector For Multi-Threaded Programs” ACM Transactions On Computer Systems, (Nov. 1997), V15 No. 4, pp 391-411.
Leino K. Rustan M.
Millstein Todd David
Saxe James B.
Dam Tuan
Hewlett--Packard Development Company, L.P.
Yigdall Michael
LandOfFree
System and method for verifying computer program correctness... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with System and method for verifying computer program correctness..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and System and method for verifying computer program correctness... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3558185