{"id":588,"date":"2003-08-03T20:50:25","date_gmt":"2003-08-04T00:50:25","guid":{"rendered":"\/?p=588"},"modified":"-0001-11-30T00:00:00","modified_gmt":"-0001-11-30T04:00:00","slug":"types_and_model_checking","status":"publish","type":"post","link":"https:\/\/mjtsai.com\/blog\/2003\/08\/03\/types_and_model_checking\/","title":{"rendered":"Types and Model Checking"},"content":{"rendered":"<p>\n<a href=\"http:\/\/www.cs.purdue.edu\/homes\/mnaik\/pubs\/tsemc.html\">Mayur Naik and Jens Palsberg<\/a>:\n<\/p>\n\n<blockquote cite=\"http:\/\/www.cs.purdue.edu\/homes\/mnaik\/pubs\/tsemc.html\">\nType systems and model checking are two approaches to finding bugs in software. Are they equally powerful? On the surface, they are quite different: type checking works on the program itself, often in a modular fashion, while model checking works on a model of the program. Type soundness ensures that all reachable program states satisfy a certain property provided the program is well typed, while model-checking soundness guarantees the same without any assumptions about types. Thus, model checking seems to be more powerful than type checking: Type soundness essentially says that type checking implies model checking, but there are not many cases where the converse holds.&hellip;In this paper, we present a type system that is equivalent to model checking.\n<\/blockquote>","protected":false},"excerpt":{"rendered":"<p>Mayur Naik and Jens Palsberg: Type systems and model checking are two approaches to finding bugs in software. Are they equally powerful? On the surface, they are quite different: type checking works on the program itself, often in a modular fashion, while model checking works on a model of the program. Type soundness ensures that [&hellip;]<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"","sticky":false,"template":"","format":"standard","meta":{"apple_news_api_created_at":"","apple_news_api_id":"","apple_news_api_modified_at":"","apple_news_api_revision":"","apple_news_api_share_url":"","apple_news_coverimage":0,"apple_news_coverimage_caption":"","apple_news_is_hidden":false,"apple_news_is_paid":false,"apple_news_is_preview":false,"apple_news_is_sponsored":false,"apple_news_maturity_rating":"","apple_news_metadata":"\"\"","apple_news_pullquote":"","apple_news_pullquote_position":"","apple_news_slug":"","apple_news_sections":"\"\"","apple_news_suppress_video_url":false,"apple_news_use_image_component":false,"footnotes":""},"categories":[4],"tags":[],"class_list":["post-588","post","type-post","status-publish","format-standard","hentry","category-programming-category"],"apple_news_notices":[],"_links":{"self":[{"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/posts\/588","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/comments?post=588"}],"version-history":[{"count":0,"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/posts\/588\/revisions"}],"wp:attachment":[{"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/media?parent=588"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/categories?post=588"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/tags?post=588"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}