{"id":52,"date":"2021-04-08T09:10:45","date_gmt":"2021-04-08T09:10:45","guid":{"rendered":"https:\/\/cyprusconferences.org\/mpu2022\/?page_id=52"},"modified":"2025-07-14T12:18:38","modified_gmt":"2025-07-14T12:18:38","slug":"program","status":"publish","type":"page","link":"https:\/\/cyprusconferences.org\/tase2025\/program\/","title":{"rendered":"Program"},"content":{"rendered":"

[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.22.2″ header_font=”|800|||||||” header_text_color=”#FFFFFF” header_font_size=”35px” global_colors_info=”{}”]<\/p>\n

Program<\/h1>\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 _builder_version=”4.27.4″ _module_preset=”default” global_colors_info=”{}”][et_pb_column type=”4_4″ _builder_version=”4.27.4″ _module_preset=”default” global_colors_info=”{}”][et_pb_button button_url=”https:\/\/cyprusconferences.org\/tase2025\/digital-handbook\/” url_new_window=”on” button_text=”Digital Handbook” button_alignment=”left” _builder_version=”4.27.4″ _module_preset=”default” custom_button=”on” button_text_color=”gcid-heading-color” global_colors_info=”{%22gcid-heading-color%22:%91%22button_text_color%22%93}”][\/et_pb_button][et_pb_tabs _builder_version=”4.27.4″ _module_preset=”default” hover_enabled=”0″ global_colors_info=”{}” sticky_enabled=”0″][et_pb_tab title=”Monday 14\/07″ _builder_version=”4.27.4″ _module_preset=”default” hover_enabled=”0″ global_colors_info=”{}” sticky_enabled=”0″]<\/p>\n

Monday Schedule<\/h2>\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n
Time<\/th>\nSession<\/th>\nTalk<\/th>\n<\/tr>\n
9:00 – 10:00<\/td>\nInvited talk by Konstantinos Sagonas<\/strong>
\nSession Chair: Philipp R\u00fcmmer<\/td>\n		Optimal Algorithms for Stateless Model Checking<\/td>\n<\/tr>\n
10:00 – 10:30<\/td>\nProgram Verification<\/strong>
\nSession Chair: Philipp R\u00fcmmer<\/td>\n		Testing-Based Formal Verification with Program Slicing on Functional Soundness and Completeness
\nAi Liu, Yang Liu, Shaoying Liu and Zhibin Yang<\/em><\/td>\n<\/tr>\n
Coffee break<\/td>\n<\/tr>\n
11:00 – 11:30<\/td>\nProgram Verification
\n<\/strong>Session Chair: Konstantinos Sagonas<\/td>\n		Dependent Assertion Logic for Modular Software Verification
\nLukas Gr\u00e4tz<\/em><\/td>\n<\/tr>\n
11:30 – 12:00<\/td>\nA Formal Framework for Naturally Specifying and Verifying Sequential Algorithms
\nChengxi Yang, Shushu Wu and Qinxiang Cao<\/em><\/td>\n<\/tr>\n
12:00 – 12:30<\/td>\nMachine-Checked Compositional Specification and Proofs for Embedded Systems
\nKarl Palmskog, Mattias Nyberg and Dilian Gurov<\/em><\/td>\n<\/tr>\n
Lunch break<\/td>\n<\/tr>\n
14:00 – 14:30<\/td>\nVerification and Concurrency<\/strong>
\nSession Chair: Shaoying Liu<\/td>\n		Failure divergence refinement for Event-B
\nSebastian Stock, Michael Leuschel and Atif Mashkoor<\/em><\/td>\n<\/tr>\n
14:30 – 15:00<\/td>\nMining Diamonds in labeled Transition Systems
\nFlip van Spaendonck and Kevin Jilissen<\/em><\/td>\n<\/tr>\n
15:00 – 15:30<\/td>\nPortability of Optimizations from SC to TSO
\nAkshay Gopalakrishnan and Clark Verbrugge<\/em><\/td>\n<\/tr>\n
Coffee break<\/td>\n<\/tr>\n
16:00 – 16:30<\/td>\nSAT and SMT Solving<\/strong>
\nSession Chair: Lucas C. Cordeiro<\/td>\n		Adaptive Clause Management in SMT Solvers: A Dynamic Weighting Framework for Formal Verification
\nWenda Leng, Meihua Liu and Yufeng Jin<\/em><\/td>\n<\/tr>\n
16:30 – 17:00<\/td>\nSNRWLS: Improve (W)PMS Solver with Weighting Strategies Related to Number of Soft Clauses
\nChen Shuhao, Jiang Menghua and Chen Yin<\/em><\/td>\n<\/tr>\n
19:00 – 20:30<\/td>\nWelcome Reception<\/strong><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

 [\/et_pb_tab][et_pb_tab title=”Tuesday 15\/07″ _builder_version=”4.27.4″ _module_preset=”default” hover_enabled=”0″ global_colors_info=”{}” sticky_enabled=”0″]<\/p>\n

Tuesday Schedule<\/h2>\n\n\n\n\n\n\n\n\n\n\n\n\n\n
Time<\/th>\nSession<\/th>\nTalk<\/th>\n<\/tr>\n
9:00 – 10:00<\/td>\nInvited talk by Min Zhang<\/strong>
Session Chair: Zhilin Wu<\/td>\n		Safeguarding deep reinforcement learning systems via formal methods: From safety-by-design to runtime assurance<\/td>\n<\/tr>\n
10:00 – 10:30<\/td>\nTrustworthy AI and System Software
<\/strong>Session Chair: Zhilin Wu<\/td>\n		Robust Deep Reinforcement Learning Using Formal Verification
Avraham Raviv, Shaiel Vistuch, Erel Dekel, Boaz Gurevich and Hillel Kugler<\/em><\/td>\n<\/tr>\n
Coffee break<\/td>\n<\/tr>\n
11:00 – 11:30<\/td>\nTrustworthy AI and System Software
<\/strong>Session Chair: Min Zhang<\/td>\n		A Formally Verified Neural Network Converter for the Interactive Theorem Prover Coq
Leo Alexander Gummersbach, Kim V\u00f6llinger and Andrei Aleksandrov<\/em><\/td>\n<\/tr>\n
11:30 – 12:00<\/td>\nCOMPASS: An Agent for MLIR Compilation Pass Pipeline Generation
Hongbin Zhang, Shihao Gao, Yang Liu, Mingjie Xing, Yanjun Wu and Chen Zhao<\/em><\/td>\n<\/tr>\n
12:00 – 12:30<\/td>\nStable Ranges: Shared Dichotomy in Large Version-Controlled Repositories
Laurent Bulteau, Pierre-Yves David, Florian Horn and Euxane Tran-Girard<\/em><\/td>\n<\/tr>\n
Lunch break<\/td>\n<\/tr>\n
14:00 – 14:30<\/td>\nProgram Analysis using ML<\/strong>
Session Chair: Hillel Kugler<\/td>\n		CASTLE: Benchmarking Dataset for Static Code Analyzers and LLMs towards CWE Detection
Richard A. Dubniczky, Krisztofer Zolt\u00e1n Horv\u00e1t, Tam\u00e1s Bisztray, Mohamed Amine Ferrag, Lucas C. Cordeiro and Norbert Tihanyi<\/em><\/td>\n<\/tr>\n
14:30 – 15:00<\/td>\nFAMiT: Mitigating False Alarms for Program Analysis Using Large Language Models (Short paper)
Jiabao Zeng, Yuanlin Li, Ran Zhang, Yuanmin Xie, Kejia Li and Min Zhou<\/em><\/td>\n<\/tr>\n
17:15<\/td>\nTour & Dinner<\/strong><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

 <\/p>\n

[\/et_pb_tab][et_pb_tab title=”Wednesday 16\/07″ _builder_version=”4.27.4″ _module_preset=”default” global_colors_info=”{}”]<\/p>\n

Wednesday Schedule<\/h2>\n\n\n\n\n\n\n\n\n\n\n
Time<\/th>\nSession<\/th>\nTalk<\/th>\n<\/tr>\n
9:00 – 9:30<\/td>\nSecurity<\/strong>
Session Chair: Karl Palmskog<\/td>\n		A Cross-domain Data Sharing Scheme Based on Federated Blockchain
Honglin Mao, Jie Zhang, Yao Zhang and Xiaohong Li<\/em><\/td>\n<\/tr>\n
9:30 – 10:00<\/td>\nOperational Semantics for Crystality: A Smart Contract Language for Parallel EVMs
Ziyun Xu, Hao Wang and Meng Sun<\/em><\/td>\n<\/tr>\n
10:00 – 10:30<\/td>\nDetecting speculative data flow vulnerabilities using weakest precondition reasoning
Graeme Smith<\/em><\/td>\n<\/tr>\n
Coffee break<\/td>\n<\/tr>\n
11:00 – 11:30<\/td>\nDynamic Analysis<\/strong>
Session Chair: Graeme Smith<\/td>\n		Random Testing of Model Checkers for Timed Automata with Automated Oracle Generation
Andrea Manini, Matteo Rossi and Pierluigi San Pietro<\/em><\/td>\n<\/tr>\n
11:30 – 12:00<\/td>\nState Significance-Guided Fuzzing for Stateful Protocol Program
Kunpeng Jian, Yanyan Zou, Chen Wang, Ning Li, Menghao Li and Wei Huo<\/em><\/td>\n<\/tr>\n
12:00 – 12:30<\/td>\nUnleash the Hidden Power of CAR-based Model Checking through Dynamic Traversal
Yibo Dong, Yu Chen, Jianwen Li and Geguang Pu<\/em><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

[\/et_pb_tab][\/et_pb_tabs][\/et_pb_column][\/et_pb_row][\/et_pb_section]<\/p>\n","protected":false},"excerpt":{"rendered":"

ProgramMonday Schedule Time Session Talk 9:00 – 10:00 Invited talk by Konstantinos Sagonas Session Chair: Philipp R\u00fcmmer Optimal Algorithms for Stateless Model Checking 10:00 – 10:30 Program Verification Session Chair: Philipp R\u00fcmmer Testing-Based Formal Verification with Program Slicing on Functional Soundness and Completeness Ai Liu, Yang Liu, Shaoying Liu and Zhibin Yang Coffee break 11:00 – 11:30 Program Verification Session Chair: Konstantinos Sagonas Dependent Assertion Logic for Modular Software Verification Lukas Gr\u00e4tz 11:30 – 12:00 A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms Chengxi Yang, Shushu Wu and Qinxiang Cao 12:00 – 12:30 Machine-Checked Compositional Specification and Proofs for Embedded Systems Karl Palmskog, Mattias Nyberg and Dilian Gurov Lunch break 14:00 – 14:30 Verification and Concurrency Session Chair: Shaoying Liu Failure divergence refinement for Event-B Sebastian Stock, Michael Leuschel and Atif Mashkoor 14:30 – 15:00 Mining Diamonds in labeled Transition Systems Flip van Spaendonck and Kevin Jilissen 15:00 – 15:30 Portability of Optimizations from SC to TSO Akshay Gopalakrishnan and Clark Verbrugge Coffee break 16:00 – 16:30 SAT and SMT Solving Session Chair: Lucas C. Cordeiro Adaptive Clause Management in SMT Solvers: A Dynamic Weighting Framework for Formal Verification Wenda Leng, Meihua Liu and Yufeng Jin 16:30 – […]<\/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\/52"}],"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=52"}],"version-history":[{"count":39,"href":"https:\/\/cyprusconferences.org\/tase2025\/wp-json\/wp\/v2\/pages\/52\/revisions"}],"predecessor-version":[{"id":244286,"href":"https:\/\/cyprusconferences.org\/tase2025\/wp-json\/wp\/v2\/pages\/52\/revisions\/244286"}],"wp:attachment":[{"href":"https:\/\/cyprusconferences.org\/tase2025\/wp-json\/wp\/v2\/media?parent=52"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}