Escher C Verifier
Escher C Verifier (or eCv for short) is a tool
for developing formally-verified C code for safety-critical
and other high-integrity software systems.
What is so special about eCv?
Unlike traditional static analysis tools, eCv verifies software so
that it is mathematically proven to be free from run-time errors.
Even better, you can use eCv to prove that your software satisfies any safety
properties, or other functional specifications, that you provide.
The proofs take account of all possible inputs.
This is clearly preferable to hoping that sufficient input data is used during
testing to detect every error in the software.
eCv uses the same mature automated theorem
prover as Perfect Developer. This prover has been developed over
many years so that it is able to prove all or nearly all true verification
conditions without user intervention.
How does eCv work?
It works by adapting C and C++ like this:
- First, we subset the language to remove
unsafe features, using MISRA-C 2004 as a basis;
- Then we strengthen the type system
to give you the benefits of a strongly-typed language;
- Next, we add preconditions and
other constructs to support
Verified Design-by-Contract;
- This allows eCv to verify
the program using a powerful automatic theorem prover.
All the above is done in such a way that your eCv program is
still a valid C or C++ program, so that it can be compiled using a standard compiler.
|
TOP
