Formal Verification of C and C++ ?

I haven't checked these out yet, but they look interesting...

Formal Verification of C and C++

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
• 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?

Escher Technologies - Articles

'via Blog this'