# Difference between revisions of "Formal Methods and Theorem Provers"

From T-VEC Wiki

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 11:58, 14 January 2007

T-VEC is a formal method.

Formal methods are mathematically-based techniques for the specification, development and verification of software and hardware systems.

See http://en.wikipedia.org/wiki/Formal_methods

T-VEC (behind the scenes is a Theorem Prover) - per the wiki taxonomy

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.