University of Limerick Institutional Repository

Assertion-based loop invariant generation

DSpace Repository

Show simple item record

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


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search DSpace


Browse

My Account

Statistics