Verifying Code and Its Optimizations: An Experience Report

We present our experience in formally verifying the correctness of a 200-line industrial C implementation of Cyclic Redundancy Check (CRC) and its optimizations. Our experience indicates that (a) both the specification and verification of even such small code can be hard to automate and needs intense manual effort, and (b) verifying certain optimizations to an existing code is relatively easier. It took us 10 days to specify and 5 days verify the correctness of this 200 line program. Our initial attempt to verify the correctness, using the model checker CBMC, did not scale up due to a huge loop unwinding (220 times). Since it is hard to scale model checking for such huge loops, we first verified each function´s correctness independently using CBMC and then verified the correctness of the loop through manual application of induction using CBMC. This traditional modular and inductive approach helped CBMC verify the implementation within 25 seconds. Furthermore, the implementation was poorly coded to begin with and had to undergo several optimizations to meet its performance requirement. With our optimizations, the CRC implementation met its performance requirement. Due to the changes in code for the optimizations, we needed to reverify the complete implementation. To lessen the verification rework, we proved one optimization at a time, in each function, by proving that the behavior of the function is preserved by the optimization. It took us 7 days to code the optimizations and 1 day to verify them. This optimized correct implementation was accepted and shipped by our client along with the client´s automotive software. In future, we would like to generalize this approach to verify behavior preserving changes, and we believe that some of these steps can be automated.