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'
No comments:
Post a Comment