Journal
ACM COMPUTING SURVEYS
Volume 46, Issue 3, Pages -Publisher
ASSOC COMPUTING MACHINERY
DOI: 10.1145/2506375
Keywords
Algorithms; Verification; Loop invariants; deductive verification; preconditions and postconditions; formal verification
Categories
Funding
- Swiss National Science Foundation [200021-134976, 200020-134974]
- Hasler Foundation
- mail.ru group
Ask authors/readers for more resources
Software verification has emerged as a key concern for ensuring the continued progress of information technology. Full verification generally requires, as a crucial step, equipping each loop with a loop invariant. Beyond their role in verification, loop invariants help program understanding by providing fundamental insights into the nature of algorithms. In practice, finding sound and useful invariants remains a challenge. Fortunately, many invariants seem intuitively to exhibit a common flavor. Understanding these fundamental invariant patterns could therefore provide help for understanding and verifying a large variety of programs. We performed a systematic identification, validation, and classification of loop invariants over a range of fundamental algorithms from diverse areas of computer science. This article analyzes the patterns, as uncovered in this study, governing how invariants are derived from postconditions; it proposes a taxonomy of invariants according to these patterns; and it presents its application to the algorithms reviewed. The discussion also shows the need for high-level specifications based on domain theory. It describes how the invariants and the corresponding algorithms have been mechanically verified using an automated program prover; the proof source files are available. The contributions also include suggestions for invariant inference and for model-based specification.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available