Benchmarking Crimes Meet Formal Verification

https://microkerneldude.org/2025/04/27/benchmarking-crimes-meet-formal-verification/

by snvzz • 1 year ago

37 6 1 year ago

Animats3• 1 year ago

Sigh.

Decades ago I headed a project to build a proof of correctness system.[1] It was for a rather dialect of Pascal for real-time engine control programs. Some of the comments I made back then still apply.

- Assertions belong in the program source, and in the same syntax as the language of the program. They're mostly written by the people writing the code. The proof of correctness work can and should be integrated with development.

- Most, but not all, of the theorem proving can be automated with what's now called a "SAT solver". We had the original Oppen-Nelson simplifier for that.

- Sometimes you need more theorem proving power than a SAT solver. We used the original Boyer-Moore theorem prover for that. It's automatic, but you can help it by suggesting intermediate theorems.

- To tie complex theorems to concrete code, programmers should write

    assert(a);
    assert(b);

where a can be proved from the code above by the SAT solver, and b is what you need to prove constraints on the following code. Now you have to prove a implies b. That's when you need a more interactive prover, or one with more power. a implies b should be a statement that stands alone, without reference to other code. This allows turning the problem over to the people who are into theorem proving, while the programmers can get on with coding.

- Many of the people involved in program verification are heavily into the formalism, rather than seeing this as a way to eliminate bugs. This leads to excessive formalism. That tendency has to be restrained.

[1] https://github.com/John-Nagle/pasv

staunton• 1 year ago

Was that project a success? Was it used in practice? Was the effort justified by any usages?

The repository readme doesn't seem to go into that.

Animats3• 1 year ago

It was used a little, but the actual code that shipped in the engine controller was not written in Pascal-F, because the compiler generated inefficient code.

MaxBarraclough2• 1 year ago

Assertions belong in the program source, and in the same syntax as the language of the program. They're mostly written by the people writing the code. The proof of correctness work can and should be integrated with development.

SPARK Ada takes this approach, what do you make of it?

Animats3• 1 year ago

Looking around for examples. Google can't find anything non-trivial. Do you know of something I can look at?

Benchmarking Crimes Meet Formal Verification

Related Stories