Difference between revisions of "Formal Methods and Theorem Provers"

From T-VEC Wiki
Jump to: navigation, search
 
Line 8: Line 8:
  
 
Level 2: Theorem provers may be used to undertake fully formal machine-checked proofs. This can be very expensive and is only practically worthwhile if the cost of mistakes is extremely high (e.g., in critical parts of microprocessor design).
 
Level 2: Theorem provers may be used to undertake fully formal machine-checked proofs. This can be very expensive and is only practically worthwhile if the cost of mistakes is extremely high (e.g., in critical parts of microprocessor design).
 +
 +
===Standards===
 +
IEC61508, ISO26262 have been started to recommend Formal Method.
 +
 +
DO-178B discusses formal methods in a "soft" tone, but DO-178C is discussing it more directly.

Revision as of 10:58, 14 January 2007