{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T15:06:59Z","timestamp":1648652819421},"reference-count":16,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.79.2","type":"journal-article","created":{"date-parts":[[2012,2,20]],"date-time":"2012-02-20T22:26:05Z","timestamp":1329776765000},"page":"29-48","source":"Crossref","is-referenced-by-count":1,"title":["An Exercise in Invariant-based Programming with Interactive and Automatic Theorem Prover Support"],"prefix":"10.4204","volume":"79","author":[{"given":"Ralph-Johan","family":"Back","sequence":"first","affiliation":[{"name":"\u00c5bo Akademi University"}]},{"given":"Johannes","family":"Eriksson","sequence":"additional","affiliation":[{"name":"\u00c5bo Akademi University"}]}],"member":"2720","published-online":{"date-parts":[[2012,2,21]]},"reference":[{"issue":"3","key":"jBack08b","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/s00165-008-0070-y","article-title":"Invariant Based Programming: Basic approach and Teaching Experiences","volume":"21","author":"Ralph-Johan Back","year":"2009","journal-title":"Formal Aspects of Computing"},{"key":"inpBaErMa07","first-page":"171","article-title":"Teaching the Construction of Correct Programs Using Invariant Based Programming","volume-title":"Proc. of SEEFM 2007","author":"Ralph-Johan Back","year":"2007"},{"key":"inpBaErMy07","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-540-73770-4_4","article-title":"Testing and Verifying Invariant Based Programs in the SOCOS Environment","volume-title":"Proc. of Tests and Proofs (TAP) 2007","volume":"4454","author":"Ralph-Johan Back","year":"2007"},{"key":"inpBaMy05a","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1109\/APSEC.2005.104","article-title":"Tool Support for Invariant Based Programming","volume-title":"Proc. of APSEC 2005","author":"Ralph-Johan Back","year":"2005"},{"key":"back_preoteasa11proofrules","doi-asserted-by":"publisher","first-page":"1658","DOI":"10.1145\/1982185.1982532","article-title":"Semantics and Proof Rules of Invariant Based Programs","volume-title":"26th Symposium On Applied Computing","author":"Ralph-Johan Back","year":"2011"},{"key":"barnett_boogie:modular_2006","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","article-title":"Boogie: A modular reusable verifier for object-oriented programs","volume-title":"Proc. of FMCO 2005","volume":"4111","author":"Mike Barnett","year":"2006"},{"key":"specSharpOverview","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","article-title":"The Spec# programming system: An overview","volume-title":"CASSIS 2004","volume":"3362","author":"Mike Barnett","year":"2004"},{"key":"vandenberg01loop","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-45319-9_21","article-title":"The LOOP Compiler for Java and JML","volume-title":"Proc. of TACAS 2001","volume":"2031","author":"Joachim van den Berg","year":"2001"},{"key":"580470","volume-title":"Introduction to Algorithms","author":"Thomas H. Cormen","year":"2001"},{"issue":"3","key":"1066102","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","article-title":"Simplify: a theorem prover for program checking","volume":"52","author":"David Detlefs","year":"2005","journal-title":"Journal of the ACM"},{"issue":"2","key":"vEmden79","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1109\/TSE.1979.234171","article-title":"Programming with Verification Conditions","volume":"5","author":"M. H. van Emden","year":"1979","journal-title":"IEEE Transactions on Software Engineering"},{"key":"inpErBa10","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-16901-4_4","article-title":"Applying PVS Background Theories and Proof Strategies in Invariant Based Programming","volume-title":"Proc. of ICFEM 2010","author":"Johannes Eriksson","year":"2010"},{"key":"citeulike:2868751","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","article-title":"The Why\/Krakatoa\/Caduceus Platform for Deductive Program Verification","volume-title":"Proc. of CAV 2007","volume":"4590","author":"Jean-Christophe Filli\u00e2tre","year":"2007"},{"key":"owre96pvs","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","article-title":"PVS: Combining specification, proof checking, and model checking","volume-title":"Proc. of CAV'96","volume":"1102","author":"Sam Owre","year":"1996"},{"key":"Reynolds78","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/978-1-4612-6315-9_13","article-title":"Programming with transition diagrams","volume-title":"Programming Methodology","author":"John C. Reynolds","year":"1978"},{"issue":"9","key":"Rushby98:TSE","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1109\/32.713327","article-title":"Subtypes for Specifications: Predicate Subtyping in PVS","volume":"24","author":"John Rushby","year":"1998","journal-title":"IEEE Transactions on Software Engineering"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2017,6,20]],"date-time":"2017-06-20T10:32:45Z","timestamp":1497954765000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/1202.4829v1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,2,21]]},"references-count":16,"URL":"https:\/\/doi.org\/10.4204\/eptcs.79.2","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,2,21]]}}}