9:00 - 9:15: Opening
9:15 - 10:30: Invited talk: Sofiene Tahar: Formal Verification of Cyber-Physical Systems (Chair: Frederic Mallet)
10:30 - 11:00: Break
11:00 - 12:30: Session 1: Avionics and Spacecraft (chair: Frederic Mallet)
ˇ Neeraj Singh, Yamine Ait Ameur, Dominique Mery, David Navarre, Philippe Palanque, and Marc Pantel: Formal Development of Multi-Purpose Interactive Application (MPIA) for ARINC 661
ˇ Rodrigo Saar de Moraes and Simin Nadjm-Tehrani: Verifying Resource Adequacy of Networked IMA Systems at Concept Level
ˇ Shenghao Yuan, Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali, Tiexin Wang, and Yong Zhou: Automated Ada Code Generation from Synchronous Dataflow Programs on Multicore: Approach and Industrial Study
12:30 - 14:00: Lunch
14:00 - 15:30: Session 2: Applications (chair: Sofiene Tahar)
ˇ Dorra Ben Khalifa, Matthieu Martel, and Assale Adje: POP: A Tuning Assistant for Mixed-Precision Floating-Point Computations
ˇ Filippos Pantekis, Phillip James, Liam O'Reilly, Daniel Archambault, and Faron Moller: Visualising Railway Safety Verification
ˇ Elisabetta De Maria, Thibaud L'Yvonnet, Sabine Moisan, and Jean-Paul Rigault: Probabilistic activity recognition for serious games with applications in medicine
15:30 - 16:00: break
16:00 - 16:30: Session 3: Tools and Work in Progress (chair: Frederic Mallet)
ˇ Emily Yu, Martina Seidl, and Armin Biere: A Framework for CTLK Model Checking with QBF (Tool Paper)
ˇ Quang Thinh Trac and Mizuhito Ogawa: Formal Semantics Extraction from MIPS Instruction Manual (work in progress paper)
Workshop Program, November 16
9:45 - 10:00: Break
10:00 - 10:50: Session 1: Timing analysis (chair: Cyrille Artho)
- Qurat Ul Ain and Osman Hasan:
Formal Timing Analysis of Digital Circuits
- Étienne André:
A benchmarks library for parametric timed model checking
10:50 - 11:05: Break
11:05 - 12:20: Session 2: Decision, planning, optimization (chair: Cesar Munoz)
- Liana Mikaelyan, Sascha Müller, Andreas Gerndt and Thomas Noll:
Synthesizing and Optimizing FDIR Recovery Strategies From Fault Trees
- John Törnblom and Simin Nadjm-Tehrani:
Formal Verification of Random Forests in Safety-Critical Applications
- Maryam Kamali, Sven Linker and Michael Fisher:
Modular Verification of Vehicle Platooning with Respect to Decisions, Space and Time
12:20 - 13:30: Lunch
14:30 - 14:45: Break
14:45 - 15:35: Session 3: Refinement (chair: Osman Hasan)
- Nils Timm and Stefan Gruner:
Abstraction Refinement with Path Constraints for Three-Valued Bounded Model Checking
- Karla Morris, Colin Snook, Thai Son Hoang, Rob Armstrong and Michael Butler:
Refinement of Statecharts with Run-to-Completion Semantics
15:35 - 15:50: Coffee break
15:50 - 17:05: Session 4: Transformation and Analysis (chair: Étienne André)
- William Bombardelli Da Silva, Max Bureck, Ina Schieferdecker and Christian Hein:
Model Transformation with Triple Graph Grammars and Non-terminal Symbols
- Yuanrui Zhang, Hengyang Wu, Yxchen Chen and Frederic Mallet:
Embedding CCSL into Dynamic Logic: A Logical Approach for the Verification of CCSL Specifications
- Asad Ahmed, Osman Hasan and Falah Awwad:
Formal Stability Analysis of Control Systems
17:05 - 17:15: Closing
