Archive
Verifying loops: proving termination
If you’ve stuck with me so far in this mini-series on verifying loops, give yourself a pat on the back before reading further. When it comes to formal verification of single-threaded software, loops are the most challenging constructs to verify. Read more…
Verifying loops – part 2
Last time I showed how it was possible to analyse a loop-free and recursion-free program or function to determine its semantics (i.e. its weakest precondition and its postcondition), but that this didn’t work when we have loops. To make it possible to analyze loops thoroughly, Read more…
Verifying loops in C and C++ (intro)
When it comes to formal verification of single-threaded programs, one of the hardest constructs to verify is the humble loop. If a function contains no loops and no function calls, then a static analyser can trace through the function, looking for constructs (such as indexing an array, or dividing one number by another) that have an implied precondition Read more…
Need help with using C or C++ in critical systems? Click on my picture above.
Latest posts
- Verifying the Liskov Substitution Principle in C++ code: Part 1
- Escher C Verifier released!
- Verifying programs that use function pointers
- eCv beta 1 released!
- Verifying programs that use ‘sizeof’
- ArC is now eCv!
- Dynamic Memory Allocation in Critical Embedded Systems
- Verifying pointer arithmetic
- Run-time checks: Are they worth it?
- Aliasing and how to control it
- Verifying absence of integer overflow
- Specification with Ghost Functions
- Expressing the Inexpressible
- Verifying a binary search, part 2
- Verifying a binary search
Categories
Pages
Archives
- March 2015 (1)
- October 2011 (1)
- September 2011 (1)
- December 2010 (2)
- September 2010 (1)
- July 2010 (3)
- June 2010 (2)
- May 2010 (4)
- April 2010 (2)
- March 2010 (8)
- February 2010 (10)
- January 2010 (1)
David Crocker's Verification Blog 