Verifying Code and Its Optimizations: An Experience Report
The authors present their experience in formally verifying the correctness of a 200-line industrial C implementation of Cyclic Redundancy Check (CRC) and its optimizations. Their experience indicates that both the specification and verification of even such small code can be hard to automate and needs intense manual effort, and verifying certain optimizations to an existing code is relatively easier. It took one 10 days to specify and 5 days verify the correctness of this 200 line program. Since it is hard to scale model checking for such huge loops, they first verified each function's correctness independently using CBMC and then verified the correctness of the loop through manual application of induction using CBMC.