{"id":11,"date":"2011-11-16T07:00:34","date_gmt":"2011-11-16T07:00:34","guid":{"rendered":"http:\/\/newrsbook.cs.aau.dk\/?page_id=11"},"modified":"2022-11-10T08:47:03","modified_gmt":"2022-11-10T08:47:03","slug":"introduction","status":"publish","type":"page","link":"https:\/\/rsbook.cs.aau.dk\/","title":{"rendered":"Introduction"},"content":{"rendered":"\n<div class=\"wp-block-media-text alignwide has-media-on-the-right is-stacked-on-mobile is-vertically-aligned-center\" style=\"grid-template-columns:auto 33%\"><div class=\"wp-block-media-text__content\">\n<div class=\"wp-block-group is-layout-flow wp-block-group-is-layout-flow\" style=\"padding-top:2em;padding-right:2em;padding-bottom:2em;padding-left:2em\">\n<p><em>&#8220;Formal methods is a term used to describe the specification and verification of software systems and software using mathematical logic. There are many books that look at particular methodologies for such systems, for example, this book offers a more balanced introduction for graduate students that describes the various approaches, their strengths and weaknesses, and when they are best used. This book emerged from a variety of courses taught in Iceland and Denmark and is designed to give students a broad introduction to the area, with exercises throughout.&#8221;<\/em><\/p>\n\n\n\n<p>Welcome to the homepage for the book &#8220;Reactive Systems: Modelling, Specification and Verification&#8221;. The book has been used for courses on modelling and verification of reactive systems at several universities (<a title=\"Lectures and Slides\" href=\"https:\/\/rsbook.cs.aau.dk\/?page_id=45\" rel=\"nofollow\">here<\/a> is a list of some of them).<\/p>\n\n\n\n<p><strong>If you are using the book for one of your courses<\/strong>, please send us <a title=\"Contact\" href=\"https:\/\/rsbook.cs.aau.dk\/?page_id=28\" rel=\"nofollow\">an email<\/a> with the name of the course, its level and a URL pointing to the web-page for the course. We would like to keep track of our &#8220;user group&#8221;. Thank you.<\/p>\n\n\n\n<p><em>Luca Aceto, Anna Ing\u00f3lfsd\u00f3ttir, Kim Guldstrand Larsen and Jiri Srba<\/em><\/p>\n<\/div>\n<\/div><figure class=\"wp-block-media-text__media\"><img loading=\"lazy\" decoding=\"async\" width=\"350\" height=\"500\" src=\"https:\/\/rsbook.cs.aau.dk\/wp-content\/uploads\/2011\/11\/reactive-systems-large.jpg\" alt=\"\" class=\"wp-image-25 size-full\" srcset=\"https:\/\/rsbook.cs.aau.dk\/wp-content\/uploads\/2011\/11\/reactive-systems-large.jpg 350w, https:\/\/rsbook.cs.aau.dk\/wp-content\/uploads\/2011\/11\/reactive-systems-large-210x300.jpg 210w\" sizes=\"auto, (max-width: 350px) 100vw, 350px\" \/><\/figure><\/div>\n","protected":false},"excerpt":{"rendered":"","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-11","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/rsbook.cs.aau.dk\/index.php?rest_route=\/wp\/v2\/pages\/11","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/rsbook.cs.aau.dk\/index.php?rest_route=\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/rsbook.cs.aau.dk\/index.php?rest_route=\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/rsbook.cs.aau.dk\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/rsbook.cs.aau.dk\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=11"}],"version-history":[{"count":13,"href":"https:\/\/rsbook.cs.aau.dk\/index.php?rest_route=\/wp\/v2\/pages\/11\/revisions"}],"predecessor-version":[{"id":134,"href":"https:\/\/rsbook.cs.aau.dk\/index.php?rest_route=\/wp\/v2\/pages\/11\/revisions\/134"}],"wp:attachment":[{"href":"https:\/\/rsbook.cs.aau.dk\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=11"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}