Escher Technologies

articles

This collection of articles, mostly about formal verification of C and C++ embedded software, is based on certain posts that I originally made in my Verification Blog. They're reproduced here for convenience, and a few have been updated since they were first written.

Search the articles for:

eCv - Verified Design by Contract for C Software

Escher C Verifier (eCv) is part of Escher Verification Studio.

eCv provides formal verification of MISRA-C code by applying the principles of Verified Design by Contract.

Escher C Verifier and our flagship product Perfect Developer (PD) use the same theorem prover.

To enable those customers who wish to use PD for specification, directly followed by eCv, we combined both tools into a single product - Escher Verification Studio - with PD and eCv as components of this product.

Commercial users may buy a licence for just one component or for both of them.


	Proving C and C++ programs correct with particular reference to critical embedded systems and including an Introduction to Escher C Verifier Taming pointers in C/C++ - Part 1 Using strongly-typed Booleans in C and C++ The Taming of the Pointer - Part 2 Reasoning about null-terminated strings in C/C++ Using constrained types in C Using and Abusing Unions Making sure variables are initialized Verifying loops in C and C++ - Part 1 Verifying loops - Part 2 Verifying loops - Part 3 - Proving Termination What are you trying to prove? Verifying a binary search - Part 1 Verifying a binary search - Part 2 Expressing the Inexpressible Specification with Ghost Functions Verifying absence of integer overflow Aliasing, and how to control it Verifying pointer arithmetic Verifying programs that use "sizeof" Verifying programs that use function pointers Miscellaneous Dynamic memory allocation in critical embedded systems Which is better for critical software: C or C++? Using C++ classes in critical software Safer arrays: using a C++ array class Safer explicit type conversion More reasons why C++ can be safer than C Danger - unsigned types used here! Run-time checks: are they worth it?

articles

Proving C and C++ programs correct

with particular reference to critical embedded systems

and including an Introduction to Escher C Verifier

Miscellaneous