[et_pb_section fb_built=”1″ _builder_version=”4.22.2″ background_image=”https:\/\/cyprusconferences.org\/tase2025\/wp-content\/uploads\/2023\/05\/24857899916_6d7d641e3e_o-scaled-1.jpg” background_blend=”luminosity” global_colors_info=”{}”][et_pb_row _builder_version=”4.16″ global_colors_info=”{}”][et_pb_column type=”4_4″ _builder_version=”4.16″ global_colors_info=”{}”][et_pb_text _builder_version=”4.26.0″ header_font=”|800|||||||” header_text_color=”#FFFFFF” header_font_size=”35px” global_colors_info=”{}”]<\/p>\n
[\/et_pb_text][\/et_pb_column][\/et_pb_row][\/et_pb_section][et_pb_section fb_built=”1″ _builder_version=”4.16″ global_colors_info=”{}”][et_pb_row column_structure=”1_3,2_3″ _builder_version=”4.27.4″ _module_preset=”default” global_colors_info=”{}”][et_pb_column type=”1_3″ _builder_version=”4.27.4″ _module_preset=”default” global_colors_info=”{}”][et_pb_image src=”https:\/\/cyprusconferences.org\/tase2025\/wp-content\/uploads\/2025\/05\/Kostis-Sagonas-2.jpg” title_text=”Kostis Sagonas-2″ align=”center” _builder_version=”4.27.4″ _module_preset=”default” global_colors_info=”{}”][\/et_pb_image][\/et_pb_column][et_pb_column type=”2_3″ _builder_version=”4.25.2″ _module_preset=”default” global_colors_info=”{}”][et_pb_text _builder_version=”4.27.4″ _module_preset=”default” hover_enabled=”0″ global_colors_info=”{}” sticky_enabled=”0″]<\/p>\n
Senior Lecturer\/Associate Professor<\/span> Title<\/strong> Abstract This invited talk will present a variety of recently proposed techniques for stateless model checking, focussing on DPOR algorithms that provide (different kinds of) optimality guarantees. We will review the challenges that are involved in designing such algorithms, and the time and space guarantees that some of these algorithms provide. Last, but not least, we will present SMC tools implementing these algorithms, and some results from code bases that these tools have been applied.<\/strong><\/p>\n Bio [\/et_pb_text][\/et_pb_column][\/et_pb_row][et_pb_row column_structure=”1_3,2_3″ _builder_version=”4.27.4″ _module_preset=”default” global_colors_info=”{}”][et_pb_column type=”1_3″ _builder_version=”4.27.4″ _module_preset=”default” global_colors_info=”{}”][et_pb_image src=”https:\/\/cyprusconferences.org\/tase2025\/wp-content\/uploads\/2025\/04\/Min-Zhang.jpg” title_text=”Min Zhang” align=”center” _builder_version=”4.27.4″ _module_preset=”default” global_colors_info=”{}”][\/et_pb_image][\/et_pb_column][et_pb_column type=”2_3″ _builder_version=”4.25.2″ _module_preset=”default” global_colors_info=”{}”][et_pb_text _builder_version=”4.27.4″ _module_preset=”default” global_colors_info=”{}”]<\/p>\n Full Professor Title<\/strong> Abstract Bio Keynote SpeakersKonstantinos Sagonas Senior Lecturer\/Associate ProfessorDepartment of Information Technology; Division of Computer SystemsUppsala University TitleOptimal Algorithms for Stateless Model Checking AbstractStateless model checking (SMC) is a fully automatic testing and verification technique with low memory requirements. It checks concurrent programs for safety errors (e.g. program crashes, assertion violations, etc.) by systematically exploring all possible thread schedulings. SMC becomes effective when coupled with Dynamic Partial Order Reduction (DPOR), a runtime technique which introduces an equivalence on schedulings and reduces the amount of exploration. DPOR algorithms that are \\emph{optimal} are particularly effective in that they guarantee to explore \\emph{exactly} one execution from each equivalence class, thereby avoiding redundant work and managing to achieve sometimes exponential reduction over non-optimal techniques. This invited talk will present a variety of recently proposed techniques for stateless model checking, focussing on DPOR algorithms that provide (different kinds of) optimality guarantees. We will review the challenges that are involved in designing such algorithms, and the time and space guarantees that some of these algorithms provide. Last, but not least, we will present SMC tools implementing these algorithms, and some results from code bases that these tools have been applied. BioKonstantinos Sagonas received the PhD degree in computer science […]<\/p>\n","protected":false},"author":8,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"_et_pb_use_builder":"on","_et_pb_old_content":"","_et_gb_content_width":"","footnotes":""},"_links":{"self":[{"href":"https:\/\/cyprusconferences.org\/tase2025\/wp-json\/wp\/v2\/pages\/244130"}],"collection":[{"href":"https:\/\/cyprusconferences.org\/tase2025\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/cyprusconferences.org\/tase2025\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/cyprusconferences.org\/tase2025\/wp-json\/wp\/v2\/users\/8"}],"replies":[{"embeddable":true,"href":"https:\/\/cyprusconferences.org\/tase2025\/wp-json\/wp\/v2\/comments?post=244130"}],"version-history":[{"count":10,"href":"https:\/\/cyprusconferences.org\/tase2025\/wp-json\/wp\/v2\/pages\/244130\/revisions"}],"predecessor-version":[{"id":244252,"href":"https:\/\/cyprusconferences.org\/tase2025\/wp-json\/wp\/v2\/pages\/244130\/revisions\/244252"}],"wp:attachment":[{"href":"https:\/\/cyprusconferences.org\/tase2025\/wp-json\/wp\/v2\/media?parent=244130"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}
<\/span><\/strong><\/span><\/strong>Department of Information Technology; Division of Computer Systems
Uppsala University
<\/strong><\/p>\n
Optimal Algorithms for Stateless Model Checking<\/p>\n
<\/strong>Stateless model checking (SMC) is a fully automatic testing and verification technique with low memory requirements. It checks concurrent programs for safety errors (e.g. program crashes, assertion violations, etc.) by systematically exploring all possible thread schedulings. SMC becomes effective when coupled with Dynamic Partial Order Reduction (DPOR), a runtime technique which introduces an equivalence on schedulings and reduces the amount of exploration. DPOR algorithms that are \\emph{optimal} are particularly effective in that they guarantee to explore \\emph{exactly} one execution from each equivalence class, thereby avoiding redundant work and managing to achieve sometimes exponential reduction over non-optimal techniques.<\/p>\n
<\/strong>Konstantinos Sagonas received the PhD degree in computer science from Stony Brook University, in 1996. He is a faculty member in the School of Electrical and Computer Engineering of NTUA, Greece and at the Dept. of Information Technology of Uppsala University, Sweden. His research interests include programming languages and systems, concurrency and distribution, and techniques and tools for the effective analysis, and testing of programs.<\/p>\nMin Zhang
\n<\/strong><\/h3>\n
\nSoftware Engineering Institute
\nEast China Normal University<\/strong><\/p>\n
\nSafeguarding deep reinforcement learning systems via formal methods: From safety-by-design to runtime assurance<\/p>\n
\n<\/strong>Deep neural networks (DNNs) have shown remarkable potential in decision-making and control for deep reinforcement learning (DRL) systems, yet their complexity and lack of transparency can make it challenging to ensure the safety of their hosting environments, including the systems they operate on. Drawing on our experiences, we argue that formal methods are crucial in training AI models that are not only robust but also certifiable, ensuring system safety at every stage from training to deployment. We demonstrate that integrating formal methods is essential to provide a comprehensive safety guarantee for DRL systems throughout their lifecycle.<\/p>\n
\n<\/strong>Min Zhang is a full professor at the Software Engineering Institute, East China Normal University. He earned his Ph.D. from the Japan Advanced Institute of Science and Technology in 2011 and joined East China Normal University in 2014. From 2019 to 2021, he served as a senior visiting professor at Nice University. His research interests primarily focus on formal methods for safety-critical systems, including real-time and AI-empowered systems. Recently, he has concentrated on the formal verification of deep neural networks and intelligent systems. He has co-authored over 80 papers, published in top-tier conferences such as CAV, TACAS, ASE, ICSE, NeurIPS, CVPR.[\/et_pb_text][\/et_pb_column][\/et_pb_row][\/et_pb_section]<\/p>\n","protected":false},"excerpt":{"rendered":"