|
|
|
|
|
|
by Fixnum
4666 days ago
|
|
|
For imperative languages, the most popular approach to formal proof is to add partial correctness annotations in an axiomatic semantics such as Hoare logic. I've heard that Microsoft does this to verify many properties of the Windows kernel. (I think the most popular tools are 3rd-party and proprietary at the moment.) Of course, finding the right theorems to write down is not easy either. There's currently an attempt to formalize a subset of C, with an axiomatic semantics, all the way from specification down to machine language: http://vst.cs.princeton.edu/ |
|
|