Appeal No. 2005-1860
Application No. 09/754,890
program flow control labels into sub-equations of a logical
equation called a verification condition, conditional branch
points in a program may be identified (specification, pages 3 &
4).
Representative independent claim 1 is reproduced below:
1. A method of verifying with static checking whether a
specified computer program satisfies a predefined set of
conditions, comprising:
converting the program into a logical equation representing
the predefined set of conditions as applied to instructions and
elements of the instructions of the program, the converting step
including inserting flow control labels into the sub-equations of
the logical equation, the flow control labels identifying
conditional branch points in the specified computer program;
applying a theorem prover to the logical equation to
determine the truth of the logical equation, and when the truth
of the logical equation cannot be proved, generating at least one
counter-example identifying one of the conditions, one or more
variable values inconsistent with the one condition, and any of
the flow control labels for conditional branch points of the
program associated with the identified variable values; and
converting the at least one counter-example into an error
message that includes a program trace that identifies a path
through the computer program when the counter-example identifies
one or more of the flow control labels.
The Examiner relies on the following references:
Chan et al. (Chan) 4,920,538 Apr. 24, 1990
Rickel et al. (Rickel) 5,854,924 Dec. 29, 1998
David L. Detlefs et al. (Detlefs), “Extended Static Checking,”
Compaq Systems Research Center, SRC Research report #159
(December 18, 1998), pp. 1-44.
2
Page: Previous 1 2 3 4 5 6 7 8 9 Next
Last modified: November 3, 2007