Archive
Posts Tagged ‘loop variant’
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…
Need help with using C or C++ in critical systems? Click on my picture above.
Join 30 other subscribers
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 