Escher Technologies Escher Technologies
Home Tools Services Support News Company Contact Publications Articles
Escher Technologies
More:
arrowEscher Verification Studio
arrowAbout Perfect Developer
arrowWhat others say about PD
arrowCritical software
arrowYour development process
arrowPD process overview
arrowPD and SPARK Ada
arrowSummary of benefits
arrowEvaluating the tools
eCv is written in the specification language used by Perfect Developer, and compiled to C++.
eCv - reducing the cost of developing Critical Software

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.

Interested?

If you would like some more information about eCv, please contact us. You can find the eCv product datasheet on the Publications page. And have you seen our blog about verifying C and C++ programs?

 


Home    TOPTOP
Copyright © 1997-2021 Escher Technologies Limited. All rights reserved. Information is subject to change without notice.      Link to  Privacy/Cookie Policy (new window)