{"id":1332,"date":"2021-10-01T22:43:02","date_gmt":"2021-10-01T14:43:02","guid":{"rendered":"http:\/\/lcs.ios.ac.cn\/fm2021\/?page_id=1332"},"modified":"2021-12-09T14:22:05","modified_gmt":"2021-12-09T06:22:05","slug":"main-program_est","status":"publish","type":"page","link":"http:\/\/lcs.ios.ac.cn\/fm2021\/main-program_est\/","title":{"rendered":"FM'21 Main Conference Program"},"content":{"rendered":"<div class=\"fusion-fullwidth fullwidth-box fusion-builder-row-1 fusion-flex-container nonhundred-percent-fullwidth non-hundred-percent-height-scrolling\" style=\"background-color: rgba(255,255,255,0);background-position: center center;background-repeat: no-repeat;border-width: 0px 0px 0px 0px;border-color:#e2e2e2;border-style:solid;\" ><div class=\"fusion-builder-row fusion-row fusion-flex-align-items-flex-start\" style=\"max-width:1248px;margin-left: calc(-4% \/ 2 );margin-right: calc(-4% \/ 2 );\"><div class=\"fusion-layout-column fusion_builder_column fusion-builder-column-0 fusion_builder_column_1_1 1_1 fusion-flex-column\"><div class=\"fusion-column-wrapper fusion-flex-justify-content-flex-start fusion-content-layout-column\" style=\"background-position:left top;background-repeat:no-repeat;-webkit-background-size:cover;-moz-background-size:cover;-o-background-size:cover;background-size:cover;padding: 0px 0px 0px 0px;\"><div class=\"fusion-builder-row fusion-builder-row-inner fusion-row fusion-flex-align-items-flex-start\" style=\"width:104% !important;max-width:104% !important;margin-left: calc(-4% \/ 2 );margin-right: calc(-4% \/ 2 );\"><div class=\"fusion-layout-column fusion_builder_column_inner fusion-builder-nested-column-0 fusion_builder_column_inner_1_1 1_1 fusion-flex-column fusion-flex-align-self-center\"><div class=\"fusion-column-wrapper fusion-flex-justify-content-center fusion-content-layout-row\" style=\"background-position:left top;background-repeat:no-repeat;-webkit-background-size:cover;-moz-background-size:cover;-o-background-size:cover;background-size:cover;padding: 0px 0px 0px 0px;\"><div ><style type=\"text\/css\">.fusion-button.button-1 {border-radius:4px;}<\/style><a class=\"fusion-button button-flat fusion-button-default-size button-default button-1 fusion-button-default-span fusion-button-default-type\" target=\"_self\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/main-program_est\/#Day1\"><span class=\"fusion-button-text\">Nov. 22 06:00-10:00<\/span><\/a><\/div><div ><style type=\"text\/css\">.fusion-button.button-2 {border-radius:4px;}<\/style><a class=\"fusion-button button-flat fusion-button-default-size button-default button-2 fusion-button-default-span fusion-button-default-type\" target=\"_self\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/main-program_est\/#Day2\"><span class=\"fusion-button-text\">Nov. 23 06:00-10:20<\/span><\/a><\/div><div ><style type=\"text\/css\">.fusion-button.button-3 {border-radius:4px;}<\/style><a class=\"fusion-button button-flat fusion-button-default-size button-default button-3 fusion-button-default-span fusion-button-default-type\" target=\"_self\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/main-program_est\/#Day3\"><span class=\"fusion-button-text\">Nov. 24 06:00-10:20<\/span><\/a><\/div><div ><style type=\"text\/css\">.fusion-button.button-4 {border-radius:4px;}<\/style><a class=\"fusion-button button-flat fusion-button-default-size button-default button-4 fusion-button-default-span fusion-button-default-type\" target=\"_self\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/main-program_est\/#Day4\"><span class=\"fusion-button-text\">Nov.25 06:00-08:40<\/span><\/a><\/div><div ><style type=\"text\/css\">.fusion-button.button-5 {border-radius:4px;}<\/style><a class=\"fusion-button button-flat fusion-button-default-size button-default button-5 fusion-button-default-span fusion-button-default-type\" target=\"_self\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/main-program_est\/#Day5\"><span class=\"fusion-button-text\">Nov. 26 04:00-10:20<\/span><\/a><\/div><\/div><\/div><style type=\"text\/css\">.fusion-body .fusion-builder-nested-column-0{width:100% !important;margin-top : 0px;margin-bottom : 20px;}.fusion-builder-nested-column-0 > .fusion-column-wrapper {padding-top : 0px !important;padding-right : 0px !important;margin-right : 1.92%;padding-bottom : 0px !important;padding-left : 0px !important;margin-left : 1.92%;}@media only screen and (max-width:1024px) {.fusion-body .fusion-builder-nested-column-0{width:100% !important;order : 0;}.fusion-builder-nested-column-0 > .fusion-column-wrapper {margin-right : 1.92%;margin-left : 1.92%;}}@media only screen and (max-width:640px) {.fusion-body .fusion-builder-nested-column-0{width:100% !important;order : 0;}.fusion-builder-nested-column-0 > .fusion-column-wrapper {margin-right : 1.92%;margin-left : 1.92%;}}<\/style><\/div><div class=\"fusion-text fusion-text-1\"><h5 style=\"text-align: center;\"><span style=\"color: #ff0000;\">San Francisco Time, UTC -8:00<\/span><\/h5>\n<div id=\"Day1\" style=\"text-align: center; padding: 5pt 0pt 5pt 0pt; font-size: 12pt; margin: 4pt 0pt 4pt 0pt; background-color: #d4d4d4;\">Monday, November 22nd<\/div>\n<div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">06:00<\/td>\n<td>\n<div><strong>OPENING [<a href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/monday\/Openning.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<\/div>\n<div style=\"font-size: 12pt; background-color: #d8e5e9; padding: 4pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt; color: #555;\"><span style=\"color: #666; font-weight: bold;\">06:20-07:00<\/span><span style=\"margin-left: 16pt;\">Session 1: Interactive Theorem Proving<\/span><\/div>\n<div style=\"margin: 2pt 0pt 2pt 5pt;\">\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">Chair:<\/div>\n<div style=\"display: inline-block;\">Marieke Huisman<\/div>\n<\/div>\n<div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">06:20<\/td>\n<td>\n<div><a class=\"person\">Matt Griffin and <\/a><a href=\"http:\/\/brijeshdongol.github.io\/\">Brijesh Dongol<\/a><\/div>\n<div><strong>Verifying Secure Speculation in Isabelle\/HOL [<a href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/monday\/Matt.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<div>Presenter: Matt Griffin<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">06:40<\/td>\n<td>\n<div>Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin and Philippa Gardner<\/div>\n<div><strong>Two mechanisations of WebAssembly 1.0 [<a href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/monday\/Conrad.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<div>Presenter: Conrad Watt<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<\/div>\n<div style=\"font-size: 12pt; background-color: #eeeed9; padding: 3pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt;\"><span style=\"font-weight: bold; color: #555;\">07:00-07:20<\/span><span style=\"margin-left: 14pt; padding-left: 18pt; color: #555;\">Break<\/span><\/div>\n<div>\n<div style=\"font-size: 12pt; background-color: #d8e5e9; padding: 4pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt; color: #555;\"><span style=\"color: #666; font-weight: bold;\">07:20-08:40<\/span><span style=\"margin-left: 16pt;\">Session 2: Neural Networks &amp; Active Learning<\/span><\/div>\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">Chair:<\/div>\n<div style=\"display: inline-block;\">Nils Jansen<\/div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">07:20<\/td>\n<td>\n<div>Bing Sun, Jun Sun, Ting Dai and Lijun Zhang<\/div>\n<div>\n<div><strong>Probabilistic Verification of Neural Networks Against Group Fairnes [<a href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/monday\/Bing.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<div>Presenter:Bing Sun<\/div>\n<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">07:40<\/td>\n<td>\n<div>Joseph Scott, Hammad Rehman, Trishal Sudula, Federico Mora and\u00a0<a href=\"https:\/\/ece.uwaterloo.ca\/~vganesh\">Vijay Ganesh<\/a><\/div>\n<div>\n<div><strong>BanditFuzz: Fuzzing SMT Solvers with Multi-Agent Reinforcement Learning [<a href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/monday\/Federico.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<div>Presenter: Federico Mora<\/div>\n<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">08:00<\/td>\n<td>\n<div><a href=\"https:\/\/csrs.hrl.com\/\">Alexei Kopylov<\/a>, Stefan Mitsch,\u00a0<a href=\"https:\/\/csrs.hrl.com\/\">Aleksey Nogin<\/a>\u00a0and\u00a0<a href=\"https:\/\/csrs.hrl.com\/\">Michael Warren<\/a><\/div>\n<div><strong>Formally Verified Safety Net for Waypoint Navigation Neural Network Controllers [<a href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/monday\/Stefan_Aleksey.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<div>Presenter: Stefan Mitsch,\u00a0<a href=\"https:\/\/csrs.hrl.com\/\">Aleksey Nogin<\/a><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">08:20<\/td>\n<td>\n<div>Ernst Moritz Hahn, Mateo Perez,\u00a0<a href=\"http:\/\/www.csc.liv.ac.uk\/~sven\/\">Sven Schewe<\/a>,\u00a0<a href=\"http:\/\/vlsi.colorado.edu\/~fabio\">Fabio Somenzi<\/a>,\u00a0<a href=\"http:\/\/www.ashutoshtrivedi.com\/\">Ashutosh Trivedi<\/a>\u00a0and\u00a0<a href=\"http:\/\/www.csc.liv.ac.uk\/~dominik\">Dominik Wojtczak<\/a><\/div>\n<div><strong>Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives [<a href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/monday\/Mateo.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<div>Presenter: Mateo Perez<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"font-size: 12pt; background-color: #eeeed9; padding: 3pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt;\"><span style=\"font-weight: bold; color: #555;\">08:40-09:00<\/span><span style=\"margin-left: 14pt; padding-left: 18pt; color: #555;\">Break<\/span><\/div>\n<\/div>\n<div style=\"font-size: 12pt; background-color: #d8e5e9; padding: 4pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt; color: #555;\"><span style=\"color: #666; font-weight: bold;\">09:00-10:00<\/span><span style=\"margin-left: 16pt;\">Session 3<\/span><\/div>\n<div>\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">Chair:<\/div>\n<div style=\"display: inline-block;\">Corina Pasareanu<\/div>\n<\/div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">09:00<\/td>\n<td>\n<div>Clark Barrett (joint with <a href=\"https:\/\/lcs.ios.ac.cn\/memocode21\/\"><span style=\"color: #0000ff;\">MEMOCODE<\/span><\/a>)<\/div>\n<div><strong>Domain-Specific Reasoning with Satisfiability Modulo Theories (Invited Talk) [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"https:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/monday\/Clark.mp4\">Video<\/a><\/span>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div id=\"Day2\" style=\"text-align: center; padding: 5pt 0pt 5pt 0pt; font-size: 12pt; margin: 4pt 0pt 4pt 0pt; background-color: #d4d4d4;\">Tuesday, November 23rd<\/div>\n<div style=\"font-size: 12pt; background-color: #d8e5e9; padding: 4pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt; color: #555;\"><span style=\"color: #666; font-weight: bold;\">06:00-07:00<\/span><span style=\"margin-left: 16pt;\">Session 4<\/span><\/div>\n<div>\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">Chair:<\/div>\n<div style=\"display: inline-block;\">Marieke Huisman<\/div>\n<\/div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">06:00<\/td>\n<td>\n<div>Paula Herber<\/div>\n<div><strong>Combine Forces - How to Formally Verify Informally Defined Embedded Systems (Invited Talk) [<a href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/tuesday\/session4.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"font-size: 12pt; background-color: #eeeed9; padding: 3pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt;\"><span style=\"font-weight: bold; color: #555;\">07:00-07:20<\/span><span style=\"margin-left: 14pt; padding-left: 18pt; color: #555;\">Break<\/span><\/div>\n<div style=\"font-size: 12pt; background-color: #d8e5e9; padding: 4pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt; color: #555;\"><span style=\"color: #666; font-weight: bold;\">07:20-08:40<\/span><span style=\"margin-left: 16pt;\">Session 5: Logics &amp; Theory<\/span><\/div>\n<div>\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">Chair:<\/div>\n<div style=\"display: inline-block;\">Paula Herber<\/div>\n<\/div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">07:20<\/td>\n<td>\n<div>Gal Amram,\u00a0<a href=\"http:\/\/www.cs.tau.ac.il\/~maozs\/\">Shahar Maoz<\/a>, Or Pistiner and\u00a0<a href=\"https:\/\/ringert.blogspot.com\/\">Jan Oliver Ringert<\/a><\/div>\n<div><strong>Efficient Algorithms for \u03c9-Regular Energy Games [<a href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/tuesday\/session5-talk1.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">07:40<\/td>\n<td>\n<div><a href=\"http:\/\/www.cse.iitb.ac.in\/~krishnas\">Krishna S<\/a>,\u00a0<a href=\"http:\/\/www.cse.iitb.ac.in\/~khushraj\">Khushraj Madnani<\/a>,\u00a0<a href=\"http:\/\/www.mmazojr.net\/\">Manuel Mazo Jr.<\/a>\u00a0and\u00a0<a href=\"http:\/\/www.tcs.tifr.res.in\/~pandya\">Paritosh Pandya<\/a><\/div>\n<div><strong>Generalizing Non-Punctuality for Timed Temporal Logic with Freeze Quantifiers [<a href=\"http:\/\/ftplcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/tuesday\/session5-talk2.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<div>Presenter: \u00a0<a href=\"http:\/\/www.cse.iitb.ac.in\/~khushraj\">Khushraj Madnani<\/a><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">08:00<\/td>\n<td>\n<div>Matias Scharager, Katherine Cordwell, Stefan Mitsch and\u00a0<a href=\"http:\/\/lfcps.org\/\">Andr\u00e9 Platzer<\/a><\/div>\n<div><strong>Verified Quadratic Virtual Substitution for Real Arithmetic [<a href=\"https:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/tuesday\/session5-talk3.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<div>Presenter: Matias Scharager<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">08:20<\/td>\n<td>\n<div>Rim Saddem-Yagoubi,\u00a0<a href=\"http:\/\/lip6.fr\/Pascal.Poizat\">Pascal Poizat<\/a>\u00a0and Sara Houhou<\/div>\n<div><strong>Business Processes Meet Spatial Concerns: the sBPMN Verification Framework [<a href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/tuesday\/session5-talk4.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"font-size: 12pt; background-color: #eeeed9; padding: 3pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt;\"><span style=\"font-weight: bold; color: #555;\">08:40-09:00<\/span><span style=\"margin-left: 14pt; padding-left: 18pt; color: #555;\">Break<\/span><\/div>\n<div style=\"font-size: 12pt; background-color: #d8e5e9; padding: 4pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt; color: #555;\"><span style=\"color: #666; font-weight: bold;\">09:00-10:20<\/span><span style=\"margin-left: 16pt;\">Session 6: Program Verification \u2160<\/span><\/div>\n<div>\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">Chair:<\/div>\n<div style=\"display: inline-block;\">Anton Wijs<\/div>\n<\/div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">09:00<\/td>\n<td>\n<div><a href=\"https:\/\/www.kent.ac.uk\/computing\/people\/3126\/batty-mark\">Mark Batty<\/a>,\u00a0<a href=\"http:\/\/brijeshdongol.github.io\/\">Brijesh Dongol<\/a>\u00a0and Daniel Wright<\/div>\n<div><strong>Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"https:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/tuesday\/Owicki.mp4\">Video<\/a><\/span>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">09:20<\/td>\n<td>\n<div>Jinting Bian,\u00a0<a href=\"http:\/\/www.hansdieterhiep.nl\/\">Hans-Dieter Hiep<\/a>, Frank De Boer and\u00a0<a href=\"http:\/\/homepages.cwi.nl\/~frb\/\">Stijn De Gouw<\/a><\/div>\n<div><strong>Integrating ADTs in KeY and their Application to History-based Reasoning [<a href=\"https:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/tuesday\/Integrating_ADT.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">09:40<\/td>\n<td>\n<div>Alexandra Bugariu, Arshavir Ter-Gabrielyan and Peter M\u00fcller<\/div>\n<div><strong>Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers [<a href=\"https:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/tuesday\/Identifying_Overly.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">10:00<\/td>\n<td>\n<div>Nicholas Coughlin, Kirsten Winter and\u00a0<a href=\"http:\/\/www.itee.uq.edu.au\/~smith\">Graeme Smith<\/a><\/div>\n<div><strong>Rely\/guarantee reasoning for multicopy atomic weak memory models [<a href=\"https:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/tuesday\/RG_reasoning.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<div>Presenter: Nicholas Coughlin<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div id=\"Day3\" style=\"text-align: center; padding: 5pt 0pt 5pt 0pt; font-size: 12pt; margin: 4pt 0pt 4pt 0pt; background-color: #d4d4d4;\">Wednesday, November 24th<\/div>\n<div style=\"font-size: 12pt; background-color: #d8e5e9; padding: 4pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt; color: #555;\"><span style=\"color: #666; font-weight: bold;\">06:00-07:00<\/span><span style=\"margin-left: 16pt;\">Session 7<\/span><\/div>\n<div>\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">Chair:<\/div>\n<div style=\"display: inline-block;\">Ana Cavalcanti<\/div>\n<\/div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">07:00<\/td>\n<td>\n<div>FME Fellow [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/wednesday\/FME.mp4\"><strong>Video<\/strong><\/a><\/span>]<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"font-size: 12pt; background-color: #eeeed9; padding: 3pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt;\"><span style=\"font-weight: bold; color: #555;\">07:00-07:20<\/span><span style=\"margin-left: 14pt; padding-left: 18pt; color: #555;\">Break<\/span><\/div>\n<div style=\"font-size: 12pt; background-color: #d8e5e9; padding: 4pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt; color: #555;\"><span style=\"color: #666; font-weight: bold;\">07:20-08:40<\/span><span style=\"margin-left: 16pt;\">Session 8: Hybrid Systems<\/span><\/div>\n<div>\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">Chair:<\/div>\n<div style=\"display: inline-block;\">Tarmo Uustalu<\/div>\n<\/div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">07:20<\/td>\n<td>\n<div>Sota Sato, Atsuyoshi Saimen<a href=\"https:\/\/ringert.blogspot.com\/\">,\u00a0<\/a><a href=\"http:\/\/www.fos.kuis.kyoto-u.ac.jp\/~mwaga\/\">Masaki Waga<\/a>, Kenji Takao and\u00a0<a href=\"http:\/\/group-mmm.org\/~ichiro\">Ichiro Hasuo<\/a><\/div>\n<div><strong>Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: a Gas Turbine Case Study [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/wednesday\/Atsuyoshi.mp4\">Video<\/a><\/span>]<\/strong><\/div>\n<div>Presenter: Atsuyoshi Saimen<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">07:40<\/td>\n<td>\n<div>Zhenya Zhang and\u00a0<a href=\"http:\/\/group-mmm.org\/~arcaini\/\">Paolo Arcaini<\/a><\/div>\n<div><strong>Gaussian Process-Based Confidence Estimation for Hybrid System Falsification [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/wednesday\/Zhenya.mp4\">Video<\/a><\/span>]<\/strong><\/div>\n<div>Presenter: Zhenya Zhang<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">08:00<\/td>\n<td>\n<div><a href=\"http:\/\/www.uni-muenster.de\/EmbSys\">Julius Adelt<\/a>,\u00a0<a href=\"http:\/\/www.uni-muenster.de\/EmbSys\">Timm Liebrenz<\/a>\u00a0and\u00a0<a href=\"http:\/\/www.uni-muenster.de\/EmbSys\">Paula Herber<\/a><\/div>\n<div><strong>Formal Verification of Intelligent Hybrid Systems that are modeled with Simulink and the Reinforcement Learning Toolbox [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/wednesday\/Julius.mp4\">Video<\/a><\/span>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">08:20<\/td>\n<td>\n<div>Simon Foster, Mario Gleirscher, Jonathan Huerta Y Munive and\u00a0<a href=\"http:\/\/www.dcs.shef.ac.uk\/~georg\">Georg Struth<\/a><\/div>\n<div><strong>Hybrid Systems Verification with Isabelle\/HOL: Simpler Syntax, Better Models, Faster Proofs [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/wednesday\/Jonathan.mp4\">Video<\/a><\/span>]<\/strong><\/div>\n<div>Presenter: Jonathan Huerta Y Munive<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"font-size: 12pt; background-color: #eeeed9; padding: 3pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt;\"><span style=\"font-weight: bold; color: #555;\">08:40-09:00<\/span><span style=\"margin-left: 14pt; padding-left: 18pt; color: #555;\">Break<\/span><\/div>\n<div>\n<div style=\"font-size: 12pt; background-color: #d8e5e9; padding: 4pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt; color: #555;\"><span style=\"color: #666; font-weight: bold;\">09:00-10:20<\/span><span style=\"margin-left: 16pt;\">Session 9: Program Verification \u2161<\/span><\/div>\n<div>\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">Chair:<\/div>\n<div style=\"display: inline-block;\">Dorel Lucanu<\/div>\n<\/div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">09:00<\/td>\n<td>\n<div>Federico Mora, Murphy Berzish, Mitja Kulczynski,\u00a0<a href=\"http:\/\/zs.uni-kiel.de\/en\/team\/nowotka\">Dirk Nowotka<\/a>\u00a0and\u00a0<a href=\"https:\/\/ece.uwaterloo.ca\/~vganesh\">Vijay Ganesh<\/a><\/div>\n<div><strong>Z3str4: A Multi-armed String Solver [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/wednesday\/Federico.mp4\">Video<\/a><\/span>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">09:20<\/td>\n<td>\n<div>Felix A. Wolf, Malte Schwerhoff and\u00a0<a href=\"http:\/\/www.pm.inf.ethz.ch\/people\/personal\/pmueller-pers.html\">Peter M\u00fcller<\/a><\/div>\n<div><strong>Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/wednesday\/Felix.mp4\">Video<\/a><\/span>]<\/strong><\/div>\n<div>Presenter: Felix A. Wolf<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">09:40<\/td>\n<td>\n<div>\n<div>Adel Djoudi, Martin Hana and\u00a0<a href=\"https:\/\/nikolai-kosmatov.eu\/\">Nikolai Kosmatov<\/a><\/div>\n<div><strong>Formal verification of a JavaCard virtual machine with Frama-C [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/wednesday\/Adel.mp4\">Video<\/a><\/span>]<\/strong><\/div>\n<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">10:00<\/td>\n<td>\n<div><a href=\"http:\/\/franck44.github.io\/\">Franck Cassez<\/a><\/div>\n<div><strong>Verification of the Incremental Merkle Tree Algorithm with Dafny [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/wednesday\/Franck.mp4\">Video<\/a><\/span>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<\/div>\n<div id=\"Day4\" style=\"text-align: center; padding: 5pt 0pt 5pt 0pt; font-size: 12pt; margin: 4pt 0pt 4pt 0pt; background-color: #d4d4d4;\">Thursday, November 25th<\/div>\n<div style=\"font-size: 12pt; background-color: #d8e5e9; padding: 4pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt; color: #555;\"><span style=\"color: #666; font-weight: bold;\">06:00-07:00<\/span><span style=\"margin-left: 16pt;\">Session 10<\/span><\/div>\n<div>\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">Chair:<\/div>\n<div style=\"display: inline-block;\">Stefania Gnesi<\/div>\n<\/div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">07:00<\/td>\n<td>\n<div>Assia Mahboubi<\/div>\n<div><strong>Formal verification of computational mathematics (Invited Talk) [<a href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/thursday\/Assia.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"font-size: 12pt; background-color: #eeeed9; padding: 3pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt;\"><span style=\"font-weight: bold; color: #555;\">07:00-07:20<\/span><span style=\"margin-left: 14pt; padding-left: 18pt; color: #555;\">Break<\/span><\/div>\n<div style=\"font-size: 12pt; background-color: #d8e5e9; padding: 4pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt; color: #555;\"><span style=\"color: #666; font-weight: bold;\">07:20-08:40<\/span><span style=\"margin-left: 16pt;\">Session 11: Automata<\/span><\/div>\n<div>\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">Chair:<\/div>\n<div style=\"display: inline-block;\">Radu Mateescu<\/div>\n<\/div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">07:20<\/td>\n<td>\n<div><a href=\"http:\/\/iscasmc.ios.ac.cn\/?page_id=1141\">Yong Li<\/a>,\u00a0<a href=\"http:\/\/www.im.ntu.edu.tw\/~tsay\/\">Yih-Kuen Tsay<\/a>,\u00a0<a href=\"http:\/\/iscasmc.ios.ac.cn\/?page_id=152\">Andrea Turrini<\/a>,\u00a0<a href=\"http:\/\/www.cs.rice.edu\/~vardi\">Moshe Vardi<\/a>\u00a0and Lijun Zhang<\/div>\n<div><strong>Congruence Relations for B\u00fcchi Automata [<a href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/thursday\/Yong.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">07:40<\/td>\n<td>\n<div><a href=\"http:\/\/fmt.isti.cnr.it\/~mtbeek\/\">Maurice ter Beek<\/a>,\u00a0<a href=\"https:\/\/haslab.uminho.pt\/mgc\/\">Guillermina Cledou<\/a>,\u00a0<a href=\"https:\/\/www.sosy-lab.org\/people\/hennicker\/\">Rolf Hennicker<\/a>\u00a0and\u00a0<a href=\"https:\/\/jose.proenca.org\/\">Jos\u00e9 Proen\u00e7a<\/a><\/div>\n<div><strong>Featured Team Automata [<a href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/thursday\/Guillermina.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<div>Presenter: <a href=\"https:\/\/haslab.uminho.pt\/mgc\/\">Guillermina Cledou<\/a><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">08:00<\/td>\n<td>\n<div><a href=\"http:\/\/amavridou.com\/\">Anastasia Mavridou<\/a>, Andreas Katis,\u00a0<a href=\"http:\/\/ti.arc.nasa.gov\/profile\/dimitra\/\">Dimitra Giannakopoulou<\/a>, David Kooi,\u00a0<a href=\"https:\/\/ti.arc.nasa.gov\/dev\/profile\/ttp\/\">Thomas Pressburger<\/a>\u00a0and Michael W. Whalen<\/div>\n<div><strong>From Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRET [<a href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/thursday\/Anastasia.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">08:20<\/td>\n<td>\n<div>Andrea Pferscher and\u00a0<a href=\"http:\/\/www.ist.tugraz.at\/aichernig\">Bernhard K. Aichernig<\/a><\/div>\n<div><strong>Fingerprinting Bluetooth Low Energy Devices via Active Automata Learning [<a href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/thursday\/Andrea.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a>]<\/strong><\/div>\n<div>Presenter: Andrea Pferscher<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div id=\"Day5\" style=\"text-align: center; padding: 5pt 0pt 5pt 0pt; font-size: 12pt; margin: 4pt 0pt 4pt 0pt; background-color: #d4d4d4;\">Friday, November 26th<\/div>\n<div>\n<div style=\"font-size: 12pt; background-color: #d8e5e9; padding: 4pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt; color: #555;\"><span style=\"color: #666; font-weight: bold;\">04:00-05:00<\/span><span style=\"margin-left: 16pt;\">Session 12<\/span><\/div>\n<div>\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">Chair:<\/div>\n<div style=\"display: inline-block;\">Naijun Zhan<\/div>\n<\/div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">04:00<\/td>\n<td>\n<div>Mingsheng Ying<\/div>\n<div><strong>Model Checking for Verification of Quantum Circuits (Invited Talk) [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/friday\/Mingsheng.mp4\">Video<\/a><\/span>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"font-size: 12pt; background-color: #eeeed9; padding: 3pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt;\"><span style=\"font-weight: bold; color: #555;\">05:00-05:20<\/span><span style=\"margin-left: 14pt; padding-left: 18pt; color: #555;\">Break<\/span><\/div>\n<div style=\"font-size: 12pt; background-color: #d8e5e9; padding: 4pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt; color: #555;\"><span style=\"color: #666; font-weight: bold;\">05:20-07:00<\/span><span style=\"margin-left: 16pt;\">Session 13: Journal First Track<\/span><\/div>\n<div>\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">Chair:<\/div>\n<div style=\"display: inline-block;\">Eerke Boiten<\/div>\n<\/div>\n<div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">05:20<\/td>\n<td>\n<div>Rob Hierons<\/div>\n<div><strong>FSM quasi-equivalence testing via reduction and observing absences [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/friday\/Rob.mp4\">Video<\/a><\/span>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">05:40<\/td>\n<td>\n<div>Paul Gainer, Sven Linker, Clare Dixon, Ullrich Hustadt, Michael Fishe<\/div>\n<div><strong>Multi-scale verification of distributed synchronisation [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/friday\/Sven.mp4\">Video<\/a><\/span>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">06:00<\/td>\n<td>\n<div>Marcello M. Bersani, Matteo Soldo, Claudio Menghi, Patrizio Pelliccione &amp; Matteo Rossi<\/div>\n<div><strong>PuRSUE -from specification of robotic environments to synthesis of controllers [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/friday\/Marcello.mp4\">Video<\/a><\/span>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">06:20<\/td>\n<td>\n<div>Gavin Lowe<\/div>\n<div><strong>Discovering and correcting a deadlock in a channel implementation [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/friday\/Galvin.mp4\">Video<\/a><\/span>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">06:40<\/td>\n<td>\n<div>Marco Bozzano, Alessandro Cimatti,Cristian Mattarei<\/div>\n<div><strong>Formal reliability analysis of redundancy architectures [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/friday\/Alessandro.mp4\">Video<\/a><\/span>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"font-size: 12pt; background-color: #eeeed9; padding: 3pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt;\"><span style=\"font-weight: bold; color: #555;\">07:00-07:20<\/span><span style=\"margin-left: 14pt; padding-left: 18pt; color: #555;\">Break<\/span><\/div>\n<\/div>\n<\/div>\n<\/div>\n<\/div>\n<div style=\"font-size: 12pt; background-color: #d8e5e9; padding: 4pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt; color: #555;\"><span style=\"color: #666; font-weight: bold;\">07:20-08:40<\/span><span style=\"margin-left: 16pt;\">Session 14: Analysis of Complex Systems<\/span><\/div>\n<div>\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">Chair:<\/div>\n<div style=\"display: inline-block;\">Rosemary Monahan<\/div>\n<\/div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">07:20<\/td>\n<td>\n<div>Weijiang Hong,\u00a0<a href=\"http:\/\/zbchen.github.io\/\">Zhenbang Chen<\/a>, Yide Du and Ji Wang<\/div>\n<div><strong>Trace Abstraction-based Verification for Uninterpreted Programs [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/friday\/Weijiang.mp4\">Video<\/a><\/span>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">07:40<\/td>\n<td>\n<div>Felipe Gorostiaga and\u00a0<a href=\"http:\/\/software.imdea.org\/~cesar\">Cesar Sanchez<\/a><\/div>\n<div><strong>HStriver: a Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/friday\/Felipe.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a><\/span>]<\/strong><\/div>\n<div>Presenter: Felipe Gorostiage<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">08:00<\/td>\n<td>\n<div>Cui Su and\u00a0<a href=\"http:\/\/satoss.uni.lu\/jun\">Jun Pang<\/a><\/div>\n<div><strong>CABEAN 2.0: Efficient and Efficacious Control of Asynchronous Boolean Networks [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/friday\/Jun.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a><\/span>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">08:20<\/td>\n<td>\n<div>Ionut Tutu, Claudia Chirita and\u00a0<a href=\"https:\/\/discovery.dundee.ac.uk\/en\/persons\/jose-luiz-fiadeiro\">Jos\u00e9 Luiz Fiadeiro<\/a><\/div>\n<div><strong>Dynamic Reconfiguration via Typed Modalities [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/friday\/Ionut.mp4\">Video<\/a><\/span>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"font-size: 12pt; background-color: #eeeed9; padding: 3pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt;\"><span style=\"font-weight: bold; color: #555;\">08:40-09:00<\/span><span style=\"margin-left: 14pt; padding-left: 18pt; color: #555;\">Break<\/span><\/div>\n<div style=\"font-size: 12pt; background-color: #d8e5e9; padding: 4pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt; color: #555;\"><span style=\"color: #666; font-weight: bold;\">09:00-10:40<\/span><span style=\"margin-left: 16pt;\">Session 15: Probabilities<\/span><\/div>\n<div>\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">Chair:<\/div>\n<div style=\"display: inline-block;\">Maurice ter Beek<\/div>\n<\/div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">09:00<\/td>\n<td>\n<div><a href=\"http:\/\/pub.ist.ac.at\/~kchatterjee\/\">Krishnendu Chatterjee<\/a>, Ehsan Kafshdar Goharshady,\u00a0<a href=\"http:\/\/www.fi.muni.cz\/~xnovot18\/\">Petr Novotn\u00fd<\/a>, Ji\u0159\u00ed Z\u00e1rev\u00facky and \u0110or\u0111e \u017dikeli\u0107<\/div>\n<div><strong>On Lexicographic Proof Rules for Probabilistic Termination [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/friday\/\u0110or\u0111e.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a><\/span>]<\/strong><\/div>\n<div>Presenter: \u0110or\u0111e \u017dikeli\u0107<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">09:20<\/td>\n<td>\n<div>Franti\u0161ek Blahoudek,\u00a0<a href=\"https:\/\/mcubuktepe.github.io\/\">Murat Cubuktepe<\/a>,\u00a0<a href=\"http:\/\/www.fi.muni.cz\/~xnovot18\/\">Petr Novotn\u00fd<\/a>,\u00a0<a href=\"https:\/\/mornik.ae.illinois.edu\/\">Melkior Ornik<\/a>,\u00a0<a href=\"https:\/\/pranaythangeda.com\/\">Pranay Thangeda<\/a>\u00a0and Ufuk Topcu<\/div>\n<div><strong>Fuel in Markov Decision Processes (FiMDP): A Practical Approach to Consumption [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/friday\/Blahoudek.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a><\/span>]<\/strong><\/div>\n<div>Presenter: <a href=\"https:\/\/pranaythangeda.com\/\">Pranay Thangeda<\/a><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">09:40<\/td>\n<td>\n<div>Oyendrila Dobe,\u00a0<a href=\"http:\/\/ths.rwth-aachen.de\/people\/erika-abraham\/\">Erika Abraham<\/a>,\u00a0<a href=\"http:\/\/www.eziobartocci.com\/\">Ezio Bartocci<\/a>\u00a0and\u00a0<a href=\"http:\/\/www.cse.msu.edu\/~borzoo\">Borzoo Bonakdarpour<\/a><\/div>\n<div><strong>HyperProb: A Model Checker for Probabilistic Hyperproperties (short) [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/friday\/Dobe.mp4\">Video<\/a><\/span>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">09:50<\/td>\n<td>\n<div><a href=\"https:\/\/marcelmoos.com\/\">Marcel Moosbrugger<\/a>, Ezio Bartocci, Joost-Pieter Katoen and Laura Kov\u00e1cs<\/div>\n<div><strong>The Probabilistic Termination Tool Amber (short) [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/friday\/Marcel.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a><\/span>]<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">10:00<\/td>\n<td>\n<div><a href=\"http:\/\/www.es.mdh.se\/staff\/3552-Rong_Gu\">Rong Gu<\/a>, Cristina Seceleanu, Eduard Enoiu and Kristina Lundqvist<\/div>\n<div><strong>Model Checking Collision Avoidance of Nonlinear Autonomous Vehicle Models [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/friday\/Rong.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a><\/span>]<\/strong><\/div>\n<div>Presenter: Rong Gu<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">10:20<\/td>\n<td>\u00a0<strong style=\"font-family: inherit; font-size: inherit;\">Closing of Conference <strong> [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/main_conference\/friday\/Closing.mp4\"><span style=\"color: #0000ff;\">Video<\/span><\/a><\/span>]<\/strong><\/strong><\/p>\n<div><strong>1. Presentation of Best Paper Award<\/strong><\/div>\n<div><strong>2. Announcement on FM 2023<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<\/div><\/div><\/div><style type=\"text\/css\">.fusion-body .fusion-builder-column-0{width:100% !important;margin-top : 0px;margin-bottom : 20px;}.fusion-builder-column-0 > .fusion-column-wrapper {padding-top : 0px !important;padding-right : 0px !important;margin-right : 1.92%;padding-bottom : 0px !important;padding-left : 0px !important;margin-left : 1.92%;}@media only screen and (max-width:1024px) {.fusion-body .fusion-builder-column-0{width:100% !important;order : 0;}.fusion-builder-column-0 > .fusion-column-wrapper {margin-right : 1.92%;margin-left : 1.92%;}}@media only screen and (max-width:640px) {.fusion-body .fusion-builder-column-0{width:100% !important;order : 0;}.fusion-builder-column-0 > .fusion-column-wrapper {margin-right : 1.92%;margin-left : 1.92%;}}<\/style><\/div><style type=\"text\/css\">.fusion-body .fusion-flex-container.fusion-builder-row-1{ padding-top : 0px;margin-top : 0px;padding-right : 0px;padding-bottom : 0px;margin-bottom : 0px;padding-left : 0px;}<\/style><\/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":[],"_links":{"self":[{"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/pages\/1332"}],"collection":[{"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/comments?post=1332"}],"version-history":[{"count":47,"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/pages\/1332\/revisions"}],"predecessor-version":[{"id":1655,"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/pages\/1332\/revisions\/1655"}],"wp:attachment":[{"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/media?parent=1332"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}