FM PROGRAM
Days: Sunday, July 15th Monday, July 16th Tuesday, July 17th
Sunday, July 15th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:30 Session 101B
Chair:
Location: Maths LT2
| 09:00 | Deadlock Detection for Actor-based Coroutines (abstract) |
| 09:30 | An Algebraic Approach for Reasoning About Information Flow (abstract)   |
| 10:00 | Towards `Verifying' a Water Treatment System (abstract) |
10:30-11:00Coffee Break
11:00-12:00 Session 104B: FM Invited Talk: Annabelle McIver
Chair:
Location: Maths LT2
| 11:00 | Privacy in Text Processing: An information flow perspective (abstract) |
12:30-14:00Lunch Break
15:00-15:30 Session 107A
Chair:
Location: Maths LT2
| 15:00 | A Weakness Measure for GR(1) Formulae (abstract) |
15:30-16:00Coffee Break
16:00-18:00 Session 108B
Chair:
Location: Maths LT2
| 16:00 | Producing Explanations for Rich Logics (abstract) |
| 16:30 | The Compound Interest in Relaxing Punctuality (abstract) |
| 17:00 | IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems (abstract) |
| 17:30 | Timed Epistemic Knowledge Bases for Social Networks (abstract) |
Monday, July 16th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:00 Session 110B: FM Invited Talk: Leonardo de Moura
Chair:
Location: Blavatnik LT1
| 09:00 | Efficient verification and metaprogramming in Lean (abstract) |
10:00-10:30 Session 111
Chair:
Location: Blavatnik LT1
| 10:00 | Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 112B
Chair:
Location: Blavatnik LT1
| 11:00 | Encoding fairness in a synchronous concurrent program algebra (abstract) |
| 11:30 | A wide-spectrum language for verification of programs on weak memory models (abstract) |
| 12:00 | Operational Semantics of a Weak Memory Model with Channel Synchronization (abstract) |
11:00-12:30 Session 112C
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 11:00 | Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE (abstract) |
| 11:30 | Resource-aware Design for Reliable Autonomous Applications with Multiple Periods (abstract) |
| 12:00 | Verifying Auto-Generated C Code from Simulink (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 115: FLoC Plenary Lecture: Byron Cook
Chair:
Location: Maths LT1
| 14:00 | Formal Reasoning about the Security of Amazon Web Services (abstract) |
15:30-16:00Coffee Break
16:00-18:00 Session 116A: Oxford Union Debate: Ethics & Morality of Robotics
Public debate on "Ethics & Morality of Robotics" with panelists specializing in ethics, law, computer science, data security and privacy:
- Prof Matthias Scheutz, Dr Sandra Wachter, Prof Jeannette Wing, Prof Francesca Rossi, Prof Luciano Floridi & Prof Ben Kuipers
See http://www.floc2018.org/public-debate/ for further details and to register.
Location: Oxford Union
16:00-18:00 Session 116B
Chair:
Location: Blavatnik LT1
| 16:00 | QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems (abstract) |
| 16:30 | Modular Verification of Programs with Effects and Effect Handlers in Coq (abstract) |
| 17:00 | Combining Tools for Optimization and Analysis of Floating-Point Computations (abstract) |
| 17:30 | A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm (abstract) |
16:00-18:00 Session 116C
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 16:00 | Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations (abstract) |
| 16:30 | Multi-Robot LTL Planning Under Uncertainty (abstract) |
| 17:00 | Vector Barrier Certificates and Comparison Systems (abstract) |
| 17:30 | Timed Vacuity (abstract) |
19:00-21:30 FLoC banquet at Ashmolean Museum
FLoC banquet at Ashmolean Museum. Drinks and food available from 7pm (pre-booking via FLoC registration system required; guests welcome).
Location: Ashmolean Museum
Tuesday, July 17th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:30 Session 118B
Chair:
Location: Blavatnik LT1
| 09:00 | Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning (abstract) |
| 09:30 | Dynamic Symbolic Verification of MPI Programs (abstract) |
| 10:00 | To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation (abstract) |
09:00-10:30 Session 118C: FM I-Day
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 09:00 | From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems (abstract) |
| 09:30 | Interlocking Design Automation using Prover Trident (abstract) |
| 10:00 | Model-Based Testing for Avionics Systems (abstract) |
10:30-11:00Coffee Break
11:00-12:00 Session 120B: FM Invited Talk: Kim G. Larsen
Chair:
Location: Blavatnik LT1
| 11:00 | 20 Years of "Real" Real-Time Model Checking (abstract) |
12:00-12:30 Session 121
Chair:
Location: Blavatnik LT1
| 12:00 | View abstraction for systems with component identities (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 122B
Chair:
Location: Blavatnik LT1
| 14:00 | Compositional Reasoning for Shared-variable Concurrent Programs (abstract) |
| 14:30 | Statistical Model Checking of LLVM Code (abstract) |
| 15:00 | A lightweight deadlock analysis technique of object-oriented programs (abstract) |
14:00-15:30 Session 122C: FM I-Day
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 14:00 | Software Safety and Security and AI (abstract) |
| 14:30 | Variant Analysis with QL (abstract) |
| 15:00 | Object-Oriented Security Proofs (abstract) |
15:30-16:00Coffee Break
16:00-18:00 Session 123B
Chair:
Location: Blavatnik LT1
| 16:00 | CompoSAT: Specification-Guided Coverage for Model Finding (abstract) |
| 16:30 | Approximate Partial Order Reduction (abstract) |
| 17:00 | SDN-Actors: Modeling and Verification of SDN Programs (abstract) |
| 17:30 | Formal Specification and Verification of Dynamic Parametrized Architectures (abstract) |
16:00-17:30 Session 123C: FM I-Day
Chair:
Location: Blavatnik Seminar Rooms 3 & 4
| 16:00 | Z3 and SMT in Industrial R&D (abstract) |
| 16:30 | Evidential and Continuous Integration of Software Verification Tools (abstract) |
| 17:00 | Disruptive Innovations for the Development and the Deployment of Fault-Free Software (abstract) |