- Program
- Accepted Papers
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
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
