ICFEM 2022 Conference Program

Monday, October 24

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

Tuesday, October 25

  • Registration (9:15 - 9:45)
  • Welcome (9:45-10:00)
    • Adrián Riesco
  • Invited talk 1 (10:00 - 11:00)
    • Santiago Escobar
  • Break (11:00-11:30)
  • Session 1 (11:30 - 13:00) (online)
    • Ke Jiang, Tianwei Zhang, David Sanan, Yongwang Zhao and Yang Liu. A Novel Formal Methodology for Verification of 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)
    • 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)
    • 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)
    • Xiaowei Huang
  • Break (11:00-11:30)
  • Session 4 (11:30 - 13:00) (online)
    • 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)
    • 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)
    • 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)
    • Yuan Feng
  • Break (11:00-11:30)
  • Session 7 (11:30 - 13:00)
    • Robert Colvin. Separation of concerning things: a simpler basis for working with the C/C++ memory model
    • Matt Windsor and Ana Cavalcanti. RoboCert: Property Specification for RoboChart Models
    • Jaime Arias, Michał Knapik, Laure Petrucci and Wojciech Penczek. Modular Analysis of Tree-Topology Models