Loading...
Date
2007
Abstract
Many automated techniques for invariant generation are based on the idea that the invariant should show that something “bad” will not happen in the analyzed program. In this article we present an algorithm for loop invariant generation in programs with assertions using a weakest precondition calculus. We have realized the algorithm in the extended static checker ESC/Java2. Challenges stemming from our initial experience with the implementation are also discussed.
Supervisor
Description
peer-reviewed
Publisher
Citation
Proceedings of 1st International Workshop on Invariant Generation (WING 2007) collocated with the 14th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning;2007
Files
Loading...
2007_Janota.pdf
Adobe PDF, 203.26 KB
Keywords
Funding code
Funding Information
Science Foundation Ireland (SFI)
Sustainable Development Goals
External Link
Type
Meetings and Proceedings
Rights
https://creativecommons.org/licenses/by-nc-sa/1.0/