Re: Proof of Algorithm correctness
- From: Bernice Barnett <jbb@xxxxxxxxxx>
- Date: Sat, 02 Apr 2005 09:42:12 -0800
Maarten Bergvelt wrote:
>In article <1112376088.698746.302290@xxxxxxxxxxxxxxxxxxxxxxxxxxxx>,
>Deodiaus wrote:
>
>
>>Has anyone seen a "proof of algorithm correctness" for a large program.
>> Most of the proofs I have seen are for trivial small programs (e.g. a
>>sort algorithm), but want to see a proof for substantial programs. I
>>know that the problem becomes the verification of the proof and keeping
>>track of the onerous details. Oftentimes, the algorithm can be
>>incorrect, but since the person doing the proof is convinced the
>>algorithm is correct, he can be blind to errors and get lost in the
>>tedium of a proof like that.
>>I suppose that computer program have been written which "attempt" to
>>prove program correctness in certain cases, but those tend to
>>manufacture a proof, which might not be right.
>>I think it was Turning who stated that no such algorithm exists because
>>if it did then you could use it to prove itself. Thus this became an
>>inpossible aspiration.
>>
>>
>
>Maybe you should look at the work of Edsger Dijkstra, see
>http://www.cs.utexas.edu/users/EWD/. He proved the correctness of
>rather famous algorithms.
I would suggest looking at of some of the earlier publications (1960's
- 1970's) of logician/computer scientist Jon McCarthy. He and one of
his students (if memory serves me correctly) gave a correctness proof
of a compiler for a reasonable subset of the Lisp programming
language.
Other examples of large program proofs occur in the area of verified
security kernels, aka secure operating systems. The typical approach
in this case is to establish and invariant - the security policy
written in a first order language - then show that the invariant is
true initially and is true after each application of an operation
(e.g., a login or file open). The operators are usually represented by
a few first order expressions: one that describes the necessary state
when the operator is applied and one that describes the new system
state in terms of the old state and the operator parameters. More
ambitious efforts then try to prove correspondence between the model
and an implementation. Intermediate stages of proof/validation include
proofs of the consistency of the invariant and dealing with the
difference between the max and min fix points of the model.
A few products certified A1 by the Orange Book criteria (NSA) actually
used the above approaches as part oft the certification process. Do a
google search using keys "blacker" and "security" to look for some
examples.
-- Jeff Barnett
[Formatting adjusted by moderator. Please do not submit multipart email as
a newsgroup post. Flat text only, with lines under 80 characters. --djr]
.
- References:
- Proof of Algorithm correctness
- From: Deodiaus
- Re: Proof of Algorithm correctness
- From: Maarten Bergvelt
- Proof of Algorithm correctness
- Prev by Date: Even and Odd (Re: This Week's Finds in Mathematical Physics (Week 212))
- Next by Date: Re: Girsanov theorem and singular noise
- Previous by thread: Re: Proof of Algorithm correctness
- Next by thread: Contradiction found in mathematics
- Index(es):
Relevant Pages
|
Loading
