|Title||Establishing High Confidence in Code Implementations of Algorithms using Formal Verification of Pseudocode|
|Publication Type||Conference Paper|
|Year of Publication||2006|
|Authors||Archer, M., and E. Leonard|
|Conference Name||Proceedings of VERIFY'06, The Third International Verification Workshop|
|Conference Location||Seattle, Washington|
Using a theorem prover to establish that a body of code correctly implements an algorithm is a task seldom undertaken because the effort required tends to be prohibitive. Direct reasoning about code in a particular programming language requires that some version of the language's semantics---e.g., axiomatic, operational, denotational---be used to determine the program correctness assertions to establish with the theorem prover. Any scheme for generating correctness assertions will be language-specific, and for languages with complex constructs, can be complex to implement and use. Direct reasoning about algorithms using a theorem prover can be not just difficult, but impossible, if the algorithms are (as is typical) specified using informal pseudocode. This paper outlines a scheme that falls short of full program verification yet provides high confidence in the correctness of an algorithm's implementation. The scheme uses formal pseudocode specifications, in a restricted language of "while" programs with (possibly recursive) procedure calls, to bridge from algorithm specifications to implementations in code. Each block of formal pseudocode is verified in the theorem prover PVS by translating it into a state machine model and proving a set of state invariants. High confidence in implementation correctness is achieved by combining verification of the pseudocode with traceability arguments relating the algorithm specification to the pseudocode representation and the pseudocode representation to the actual code.
|NRL Publication Release Number|| |