{"id":1523,"date":"2026-02-26T20:41:10","date_gmt":"2026-02-26T20:41:10","guid":{"rendered":"https:\/\/synasc.ro\/2026\/?page_id=1523"},"modified":"2026-04-09T23:42:21","modified_gmt":"2026-04-09T23:42:21","slug":"markus-roggenbach","status":"publish","type":"page","link":"https:\/\/synasc.ro\/2026\/invited-speakers\/markus-roggenbach\/","title":{"rendered":"Markus Roggenbach"},"content":{"rendered":"\t\t<div data-elementor-type=\"wp-page\" data-elementor-id=\"1523\" class=\"elementor elementor-1523\" data-elementor-post-type=\"page\">\n\t\t\t\t<div class=\"elementor-element elementor-element-3e0b8ee e-con-full e-flex e-con e-parent\" data-id=\"3e0b8ee\" data-element_type=\"container\">\n\t\t\t\t<div class=\"elementor-element elementor-element-a3ba736 elementor-widget elementor-widget-heading\" data-id=\"a3ba736\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">Verifying Ladder Logic Programs in the Railway Domain \u2013 Theory and Practice<\/h2>\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-80ba9f5 elementor-widget elementor-widget-heading\" data-id=\"80ba9f5\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">Markus Roggenbach<\/h2>\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-7088b6b elementor-widget elementor-widget-text-editor\" data-id=\"7088b6b\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t\t\t\t\t\t<p>Swansea University, United Kingdom<\/p>\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-6af37d1 elementor-widget elementor-widget-image\" data-id=\"6af37d1\" data-element_type=\"widget\" data-widget_type=\"image.default\">\n\t\t\t\t\t\t\t\t\t\t\t\t\t\t\t<img fetchpriority=\"high\" decoding=\"async\" width=\"220\" height=\"300\" src=\"https:\/\/synasc.ro\/2026\/wp-content\/uploads\/sites\/28\/2026\/04\/MR-cropped-220x300.jpg\" class=\"attachment-medium size-medium wp-image-1564\" alt=\"\" srcset=\"https:\/\/synasc.ro\/2026\/wp-content\/uploads\/sites\/28\/2026\/04\/MR-cropped-220x300.jpg 220w, https:\/\/synasc.ro\/2026\/wp-content\/uploads\/sites\/28\/2026\/04\/MR-cropped-750x1024.jpg 750w, https:\/\/synasc.ro\/2026\/wp-content\/uploads\/sites\/28\/2026\/04\/MR-cropped-768x1048.jpg 768w, https:\/\/synasc.ro\/2026\/wp-content\/uploads\/sites\/28\/2026\/04\/MR-cropped-1125x1536.jpg 1125w, https:\/\/synasc.ro\/2026\/wp-content\/uploads\/sites\/28\/2026\/04\/MR-cropped-1501x2048.jpg 1501w, https:\/\/synasc.ro\/2026\/wp-content\/uploads\/sites\/28\/2026\/04\/MR-cropped-scaled.jpg 1876w\" sizes=\"(max-width: 220px) 100vw, 220px\" \/>\t\t\t\t\t\t\t\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-6e257af elementor-align-center elementor-hidden-widescreen elementor-hidden-desktop elementor-hidden-tablet elementor-hidden-mobile elementor-icon-list--layout-traditional elementor-list-item-link-full_width elementor-widget elementor-widget-icon-list\" data-id=\"6e257af\" data-element_type=\"widget\" data-widget_type=\"icon-list.default\">\n\t\t\t\t\t\t\t<ul class=\"elementor-icon-list-items\">\n\t\t\t\t\t\t\t<li class=\"elementor-icon-list-item\">\n\t\t\t\t\t\t\t\t\t\t\t<a href=\"#\">\n\n\t\t\t\t\t\t\t\t\t\t\t\t<span class=\"elementor-icon-list-icon\">\n\t\t\t\t\t\t\t<svg aria-hidden=\"true\" class=\"e-font-icon-svg e-fas-globe\" viewBox=\"0 0 496 512\" xmlns=\"http:\/\/www.w3.org\/2000\/svg\"><path d=\"M336.5 160C322 70.7 287.8 8 248 8s-74 62.7-88.5 152h177zM152 256c0 22.2 1.2 43.5 3.3 64h185.3c2.1-20.5 3.3-41.8 3.3-64s-1.2-43.5-3.3-64H155.3c-2.1 20.5-3.3 41.8-3.3 64zm324.7-96c-28.6-67.9-86.5-120.4-158-141.6 24.4 33.8 41.2 84.7 50 141.6h108zM177.2 18.4C105.8 39.6 47.8 92.1 19.3 160h108c8.7-56.9 25.5-107.8 49.9-141.6zM487.4 192H372.7c2.1 21 3.3 42.5 3.3 64s-1.2 43-3.3 64h114.6c5.5-20.5 8.6-41.8 8.6-64s-3.1-43.5-8.5-64zM120 256c0-21.5 1.2-43 3.3-64H8.6C3.2 212.5 0 233.8 0 256s3.2 43.5 8.6 64h114.6c-2-21-3.2-42.5-3.2-64zm39.5 96c14.5 89.3 48.7 152 88.5 152s74-62.7 88.5-152h-177zm159.3 141.6c71.4-21.2 129.4-73.7 158-141.6h-108c-8.8 56.9-25.6 107.8-50 141.6zM19.3 352c28.6 67.9 86.5 120.4 158 141.6-24.4-33.8-41.2-84.7-50-141.6h-108z\"><\/path><\/svg>\t\t\t\t\t\t<\/span>\n\t\t\t\t\t\t\t\t\t\t<span class=\"elementor-icon-list-text\">Webpage<\/span>\n\t\t\t\t\t\t\t\t\t\t\t<\/a>\n\t\t\t\t\t\t\t\t\t<\/li>\n\t\t\t\t\t\t<\/ul>\n\t\t\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-89d48db elementor-widget elementor-widget-heading\" data-id=\"89d48db\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">ABSTRACT<\/h2>\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-dd1252a elementor-widget elementor-widget-text-editor\" data-id=\"dd1252a\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t\t\t\t\t\t<p>Programmable Logic Controllers (PLCs) are used within many applications across various industries: examples include monitoring solar cells, robot control (spraying toxic chemical substances; washing the face glasses of skyscrapers), packaging and labelling systems, nuclear power plants, railway control systems.<\/p><p>The International Electrotechnical Commission specifies syntax and semantics of programming languages for such programmable controllers in its standard IEC 61131, part 3. This standard covers the graphical language &#8220;Ladder Diagrams&#8221;, often also called Ladder Logic. According to a 2022 article in the journal &#8220;Manufacturing Tomorrow&#8221;, &#8220;Ladder Logic is the main programming method used for PLCs&#8221;.<\/p><p>The invited talk will cover how to provide a formal semantics to Ladder Logic programs running on a PLC, how to define a logic expressing safety properties, and discuss various methods for verifying that a program is safe, including the IC3 algorithm. It turns out that software model checking of real-world programs is feasible, i.e., Ladder Logic verification provides a success story where a Formal Methods scales to industrial needs. Verification examples from the railway domain will illustrate the approach.<\/p>\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-8c706e9 elementor-widget elementor-widget-heading\" data-id=\"8c706e9\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">SHORT BIO<\/h2>\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-0b87dae elementor-widget elementor-widget-text-editor\" data-id=\"0b87dae\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t\t\t\t\t\t<p>Markus Roggenbach is a Professor of Computer Science at Swansea University, UK. There, he leads the interdisciplinary Swansea Centre for Research in Digital Railways as well as the Cyber Security Group in the Department of Computer Science. His research foci are formal methods for safety and for cyber security, their semantics, how to utilise them throughout the software life cycle, how to support them with tools, and their application in industrial contexts, e.g., the railway domain. He is a member of the Federation for Information Processing (IFIP) Working Group 1.3 \u201cFoundations of System Specification\u201d (chair in 2015 \u2013 2021). Markus has co-authored the book &#8220;Formal Methods for Software Engineering\u201d, Springer, 2022.<\/p>\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t","protected":false},"excerpt":{"rendered":"<p>Verifying Ladder Logic Programs in the Railway Domain \u2013 Theory and Practice Markus Roggenbach Swansea University, United Kingdom Webpage ABSTRACT Programmable Logic Controllers (PLCs) are used within many applications across various industries: examples include monitoring solar cells, robot control (spraying toxic chemical substances; washing the face glasses of skyscrapers), packaging and labelling systems, nuclear power [&hellip;]<\/p>\n","protected":false},"author":30,"featured_media":0,"parent":226,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-1523","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/pages\/1523","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/users\/30"}],"replies":[{"embeddable":true,"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/comments?post=1523"}],"version-history":[{"count":7,"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/pages\/1523\/revisions"}],"predecessor-version":[{"id":1567,"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/pages\/1523\/revisions\/1567"}],"up":[{"embeddable":true,"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/pages\/226"}],"wp:attachment":[{"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/media?parent=1523"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}