Tuesday, September 20, 2011

[vrojftdb] Two applications of proving programs correct

Formal verification:

Small, self-contained, implementation of complicated algorithm.  Easy to state program properties.

Large, distantly related parts of a program, or system, to be proved not interacting or interfering in a weird way.

Will probably need different approaches.

No comments :