ICFEM 2022 Conference Program

Monday, October 24

Workshops (please check the corresponding webpages for a detailed schedule).

• Registration (8:30 - 9:00) - Hall

Tuesday, October 25

• Registration (9:15 - 9:45) - Hall
• Welcome (9:45-10:00) - Sala de Grados
  • Adrián Riesco
• Invited talk 1 (10:00 - 11:00) - Sala de Grados
  • Santiago Escobar. Canonical Narrowing for Variant-Based Conditional Rewrite Theories
• Break (11:00-11:30)
• Session 1 (11:30 - 13:00) (online) - Sala de Grados
  • Ke Jiang, Tianwei Zhang, David Sanan, Yongwang Zhao and Yang Liu. A Formal Methodology for Verifying Side-Channel Vulnerabilities in Cache Architectures
  • Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, Thế Quyền Ngô, Thi Bich Ngoc Do and Hideaki Takai. SMT-Based Model Checking of Industrial Simulink Models
  • Zeming Wei, Xiyue Zhang and Meng Sun. Extracting Weighted Finite Automata from Recurrent Neural Networks for Natural Languages
• Lunch (13:00-14:30)
• Session 2 (14:30-16:30) - Sala de Grados
  • Sebastian Stock, Atif Mashkoor, Michael Leuschel and Alexander Egyed. Trace Refinement in B and Event-B
  • Xavier Denis, Claude Marché and Jacques-Henri Jourdan. Creusot: a Foundry for the Deductive Verification of Rust Programs
  • Graeme Smith. Declassification predicates for controlled information release
  • Wenjing Chu, Shuo Chen and Marcello Bonsangue. Non-linear optimization methods for learning regular distributions
• Break (16:30 - 17:00)
• Session 3 (17:00 - 18:30) - Sala de Grados
  • Rubén Rubio and Adrian Riesco. Theorem proving for Maude specifications using Lean
  • Giovanni Fabbretti, Ivan Lanese and Jean-Bernard Stefani. Generation of a Reversible Semantics for Erlang in Maude
  • Carlos Galindo, Sergio Perez Rubio and Josep Silva. Program slicing techniques with support for unconditional jumps

Wednesday, October 26

• Invited talk 2 (10:00 - 11:00) - Sala de Grados
  • Xiaowei Huang. Bridging Formal Methods and Machine Learning with Global Optimisation
• Break (11:00-11:30)
• Session 4 (11:30 - 13:00) (online) - Sala de Grados
  • Ran Li, Huibiao Zhu and Richard Banach. A Proof System for Cyber-physical Systems with Shared-Variable Concurrency
  • Shicheng Yi, Shuling Wang, Bohua Zhan and Naijun Zhan. Machine-checked executable semantics of Stateflow
  • Hongmeng Wang, Huan Long, Hao Wu and Qizhe Yang. On Probabilistic Extension of The Interaction Theory
• Lunch (13:00-14:30)
• Session 5 (14:30-16:30) - Sala de Grados
  • Fabian Vu, Dominik Brandt and Michael Leuschel. Model Checking B Models via High-level Code Generation
  • Alex James, Alwen Tiu and Nisansala Yatapanage. PFMC: A Parallel Symbolic Model Checker for Security Protocol Verification
  • Marko Kleine Büning, Carsten Sinz and Johannes Meuer. Refined Modularization for Bounded Model Checking through Precondition Generation
  • Paul Kogel, Verena Klös and Sabine Glesner. TTT/ik: Learning Accurate Mealy Automata Efficiently with an Imprecise Symbol Filter
• Break (16:30 - 17:00)
• Session 6 (17:00 - 18:30) (online) - Sala de Grados
  • Kangfeng Ye, Simon Foster and Jim Woodcock. Formally Verified Animation for RoboChart using Interaction Trees
  • Yuvaraj Selvaraj, Jonas Krook, Wolfgang Ahrendt and Martin Fabian. On How to Not Prove Faulty Controllers Safe in Differential Dynamic Logic
  • Imane Haur, Jean-Luc Bechennec and Olivier H. Roux. Formal verification of the inter-core synchronization of a multi-core RTOS kernel
• GALA DINNER at Metro bistro at 21:00.

Thursday, October 27

• Invited talk 3 (10:00 - 11:00) - Sala de Grados
  • Yuan Feng. Model Checking Quantum Markov Chains
• Break (11:00-11:30)
• Session 7 (11:30 - 13:00) - Sala de Grados
  • Robert Colvin. Separation of Concerning Things: A Simpler Basis for Defining and Programming with the C/C++ Memory Model
  • Matt Windsor and Ana Cavalcanti. RoboCert: Property Specification in Robotics
  • Jaime Arias, Michał Knapik, Laure Petrucci and Wojciech Penczek. Modular Analysis of Tree-Topology Models
• Lunch (13:00-14:30)