logo slogan

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