A property that is always true.
When applied to loops, it is a property that is true at both the start of a loop iteration and the end of a loop iteration.
When applied to global state, it is a property that is true at all times or when the state is not being modified (e.g., between command executions).
Notes related to Invariants
Papers related to Invariants
- Local verification of global invariants in concurrent programs [cohen:cav:2010]
- Program state abstraction for feedback-driven fuzz testing using likely invariants [fioraldi:arxiv:2020]
- Specified blocks [hehner:vstte:2008]
- Beyond the elementary representations of program invariants over algebraic data types [kostyukov:pldi:2021]
- Verifying security invariants in ExpressOS [mai:asplos:2013]
- Assertion-based encapsulation, object invariants and simulations [naumann:fmco:2004]
- A data driven approach for algebraic loop invariants [sharma:pls:2013]
- Local reasoning about while-loops [tuerk:vstte:2010]