{"id":3205,"date":"2013-04-12T05:36:10","date_gmt":"2013-04-12T05:36:10","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3205"},"modified":"2013-04-12T05:36:10","modified_gmt":"2013-04-12T05:36:10","slug":"resena-a-fully-verified-executable-ltl-model-checker","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-a-fully-verified-executable-ltl-model-checker\/","title":{"rendered":"Rese\u00f1a: A fully verified executable LTL model checker"},"content":{"rendered":"<p> Se ha publicado un art\u00edculo de verificaci\u00f3n formal con <a href=\"http:\/\/isabelle.in.tum.de\">Isabelle\/HOL<\/a> titulado <a href=\"http:\/\/www4.in.tum.de\/~nipkow\/pubs\/cav13.pdf\">A fully verified executable LTL model checker<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/www.model.in.tum.de\/~esparza\">Javier Esparza<\/a>, <a href=\"http:\/\/www21.in.tum.de\/~lammich\">Peter Lammich<\/a>, <a href=\"http:\/\/www.model.in.tum.de\/people\/detail\/index.php?id=people.detail&#038;arg=134\">Ren\u00e9 Neumann<\/a>, <a href=\"http:\/\/www4.in.tum.de\/~nipkow\">Tobias Nipkow<\/a>, <a href=\"http:\/\/www.informatik.uni-freiburg.de\/~schimpfa\">Alexander Schimpf<\/a> y <a href=\"http:\/\/www.irit.fr\/~Jan-Georg.Smaus\">Jan-Georg Smaus<\/a>.<\/p>\n<p>El trabajo se presentar\u00e1 en el <a href=\"http:\/\/cav2013.forsyte.at\">CAV 2013<\/a> (25th International Conference on Computer Aided Verification).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nWe present an LTL model checker whose code has been completely verified using the Isabelle theorem prover. The checker consists of over 4000 lines of ML code. The code is produced using recent Isabelle technology called the Refinement Framework, which allows us to split its correctness proof into (1) the proof of an abstract version of the checker, consisting of a few hundred lines of &#8220;formalized pseudocode&#8221;, and (2) a verified refinement step in which mathematical sets and other abstract structures are replaced by implementations of efficient structures like red-black trees and functional arrays. This leads to a checker that, while still slower than unverified checkers, can already be used as a trusted reference implementation against which advanced implementations can be tested. We report on the structure of the checker, the development process, and some experiments on standard benchmarks.\n<\/p><\/blockquote>\n<p>El trabajo forma parte del proyecto <a href=\"http:\/\/cava.in.tum.de\">CAVA<\/a> (Computer Aided Verification of Automata).<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas Isabelle\/HOL se encuentra <a href=\"http:\/\/cava.in.tum.de\/CAV13\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de verificaci\u00f3n formal con Isabelle\/HOL titulado A fully verified executable LTL model checker. Sus autores son Javier Esparza, Peter Lammich, Ren\u00e9 Neumann, Tobias Nipkow, Alexander Schimpf y Jan-Georg Smaus. El trabajo se presentar\u00e1 en el CAV 2013 (25th International Conference on Computer Aided Verification). Su resumen es We present an&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[1],"tags":[144,285,275],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3205"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=3205"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3205\/revisions"}],"predecessor-version":[{"id":3206,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3205\/revisions\/3206"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3205"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3205"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3205"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}