Escher Technologies Escher Technologies
Home Tools Services Support News Company Contact Publications Articles
Escher Technologies
arrowEscher Verification Studio
arrowEscher C Verifier
arrowPerfect Developer
arrowEvaluating the tools
arrowWhat others say
arrowCritical embedded software
arrowYour development process
arrowPD and SPARK Ada
arrowSummary of benefits
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 and 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.

Similarly, 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 and eCv++?

Unlike traditional static analysis tools, eCv and eCv++ verify software so that it is mathematically proven to be free from run-time errors. Even better, you can use eCv or 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 and eCv++ use 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 do eCv and eCv++ work?

They work by adapting C and C++ as follows:
  • First, we subset the C language to remove unsafe features, using MISRA-C 2012 as a basis
  • Then we strengthen the type system to give you the benefits of a strongly-typed language
  • For Escher C++ Verifier we add some C++ language constructs, carefully-chosen for safety and verifiability
  • Next, we add preconditions and other constructs to support Verified Design-by-Contract
  • These constructs allow the verifier to verify your program using a powerful automatic theorem prover

All the above is done in such a way that your program is still a valid C or C++ program, so that it can be compiled using a standard C or C++ compiler.


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


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