Accepted Papers

Robert Colvin. Separation of concerning things: a simpler basis for working with the C/C++ memory model
Giovanni Fabbretti, Ivan Lanese and Jean-Bernard Stefani. Generation of a Reversible Semantics for Erlang in Maude
Graeme Smith. Declassification predicates for controlled information release
Paul Kogel, Verena Klös and Sabine Glesner. TTT/ik: Learning Accurate Mealy Automata Efficiently with an Imprecise Symbol Filter
Kangfeng Ye, Simon Foster and Jim Woodcock. Formally Verified Animation for RoboChart using Interaction Trees
Fabian Vu, Dominik Brandt and Michael Leuschel. Model Checking B Models via High-level Code Generation
Matt Windsor and Ana Cavalcanti. RoboCert: Property Specification for RoboChart Models
Ke Jiang, Tianwei Zhang, David Sanan, Yongwang Zhao and Yang Liu. A Novel Formal Methodology for Verification of Side-channel Vulnerabilities in Cache Architectures
Wenjing Chu, Shuo Chen and Marcello Bonsangue. Non-linear optimization methods for learning regular distributions
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
Yuvaraj Selvaraj, Jonas Krook, Wolfgang Ahrendt and Martin Fabian. On How to Not Prove Faulty Controllers Safe in Differential Dynamic Logic
Shicheng Yi, Shuling Wang, Bohua Zhan and Naijun Zhan. Machine-checked executable semantics of Stateflow
Marko Kleine Büning, Carsten Sinz and Johannes Meuer. Refined Modularization for Bounded Model Checking through Precondition Generation
Ran Li, Huibiao Zhu and Richard Banach. A Proof System for Cyber-physical Systems with Shared-Variable Concurrency
Sebastian Stock, Atif Mashkoor, Michael Leuschel and Alexander Egyed. Trace Refinement in B and Event-B
Jaime Arias, Michał Knapik, Laure Petrucci and Wojciech Penczek. Modular Analysis of Tree-Topology Models
Hongmeng Wang, Huan Long, Hao Wu and Qizhe Yang. On Probabilistic Extension of The Interaction Theory
Zeming Wei, Xiyue Zhang and Meng Sun. Extracting Weighted Finite Automata from Recurrent Neural Networks for Natural Languages
Imane Haur, Jean-Luc Bechennec and Olivier H. Roux. Formal verification of the inter-core synchronization of a multi-core RTOS kernel
Xavier Denis, Claude Marché and Jacques-Henri Jourdan. Creusot: a Foundry for the Deductive Verification of Rust Programs
Rubén Rubio and Adrian Riesco. Theorem proving for Maude specifications using Lean
Alex James, Alwen Tiu and Nisansala Yatapanage. PFMC: A Parallel Symbolic Model Checker for Security Protocol Verification
Carlos Galindo, Sergio Perez Rubio and Josep Silva. Program slicing techniques with support for unconditional jumps