University of Limerick Institutional Repository
Assertion-based loop invariant generation
DSpace Repository
JavaScript is disabled for your browser. Some features of this site may not work without it.
| dc.contributor.author | Janota, Mikolas | |
| dc.date.accessioned | 2012-03-26T11:37:28Z | |
| dc.date.available | 2012-03-26T11:37:28Z | |
| dc.date.issued | 2007 | |
| dc.identifier.uri | http://hdl.handle.net/10344/2127 | |
| dc.description | peer-reviewed | en_US |
| dc.description.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. | en_US |
| dc.description.sponsorship | EC IST-2005-015905 MOBIUS project | |
| dc.language.iso | eng | en_US |
| dc.relation.ispartofseries | 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 | |
| dc.subject | JML | en_US |
| dc.subject | algorithm | en_US |
| dc.subject | java modeling language | en_US |
| dc.title | Assertion-based loop invariant generation | en_US |
| dc.type | Conference item | en_US |
| dc.type.supercollection | all_ul_research | en_US |
| dc.type.supercollection | ul_published_reviewed | en_US |
| dc.type.restriction | none | en |
| dc.contributor.sponsor | SFI | |
| dc.relation.projectid | 03/CE/2/I303_1 |
