Formal Methods and Theorem Provers

From T-VEC Wiki
Revision as of 10:56, 14 January 2007 by (Talk)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

T-VEC is a formal method.

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


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).