Using the coq theorem prover to verify complex data structure invariants
Kenneth Roe, Scott F. Smith · 2017
While automated static analysis tools can find many useful software bugs, there are still bugs that are beyond the reach of these tools. Most large software systems have complex data structures with complex invariants, and many bugs can be traced to code that does not maintain these invariants. These invariants cannot be easily inferred by automated tools. One must use an interactive system in which developers first enter these invariants to document their software and then use a theorem prover to verify their correctness.