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