{"id":1323,"date":"2017-05-15T10:04:34","date_gmt":"2017-05-15T08:04:34","guid":{"rendered":"https:\/\/www.mimuw.edu.pl\/~bojan\/?page_id=1323"},"modified":"2018-01-17T12:18:26","modified_gmt":"2018-01-17T11:18:26","slug":"linear-time-verification-and-synthesis","status":"publish","type":"page","link":"https:\/\/www.mimuw.edu.pl\/~bojan\/lipa\/lipa-summer-school\/linear-time-verification-and-synthesis","title":{"rendered":"Linear-time verification and synthesis"},"content":{"rendered":"<p>This one of the courses at the\u00a0<a href=\"https:\/\/www.mimuw.edu.pl\/~bojan\/lipa-summer-school\">Lipa Summer School<\/a>.<\/p>\n<h4>Moshe Vardi<\/h4>\n<h4><em>Linear-time verification and synthesis<\/em><\/h4>\n<p>Videos:\u00a0<a href=\"https:\/\/www.youtube.com\/watch?v=ITzDkbj_HEM\">1<\/a>,\u00a0<a href=\"https:\/\/www.youtube.com\/watch?v=Ndk_TgRXpFw\">2<\/a>,\u00a0<a href=\"https:\/\/www.youtube.com\/watch?v=KwB_cLRJPPM\">3<\/a>,\u00a0<a href=\"https:\/\/www.youtube.com\/watch?v=jqxBR1eZXMw\">4<\/a><\/p>\n<p>Algorithmic verification is one of the most successful applications of automated reasoning in computer science. In algorithmic<br \/>\nverification one uses algorithmic techniques to establish the correctness of the system under verification with respect to a given<br \/>\nproperty. Automama-theoretic Model checking is an algorithmic-verification technique that is based on a small number of key ideas, tying together graph theory, automata theory, and logic. In this self-contained tutorial I will describe how this &#8220;holy trinity&#8221; gave rise to algorithmic-verification tools, and discuss its applicability to both finite-state and infinite-state systems.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>This one of the courses at the\u00a0Lipa Summer School. Moshe Vardi Linear-time verification and synthesis Videos:\u00a01,\u00a02,\u00a03,\u00a04 Algorithmic verification is one of the most successful applications of automated reasoning in computer science. In algorithmic verification one uses algorithmic techniques to establish the correctness of the system under verification with respect to a given property. Automama-theoretic Model [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":1283,"menu_order":1,"comment_status":"closed","ping_status":"closed","template":"","meta":{"_acf_changed":false,"inline_featured_image":false,"footnotes":""},"class_list":["post-1323","page","type-page","status-publish","hentry"],"acf":[],"_links":{"self":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/1323"}],"collection":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/comments?post=1323"}],"version-history":[{"count":10,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/1323\/revisions"}],"predecessor-version":[{"id":1453,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/1323\/revisions\/1453"}],"up":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/1283"}],"wp:attachment":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/media?parent=1323"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}