Abstract
Most large software systems have complex data structures with complex invariants. Many bugs can be traced to code that does not maintain these invariants. As an example, the Heartbleed bug can be traced to an attacker sending a packet that violates an invariant that is assumed to be true in the OpenSSL code. Often these invariants are not well documented. However, maintaining them is necessary for correct operation of the software.
