FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
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 98B
Location: Blavatnik LT1
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 100B: FM Invited Talk: Annabelle McIver
Location: Blavatnik LT1
11:00
Privacy in Text Processing: An information flow perspective (abstract)
12:00-12:30 Session 101
Location: Blavatnik LT1
12:00
FSM Inference from Long Traces (abstract)
12:30-14:00Lunch Break
15:30-16:00Coffee Break
16:00-18:00 Session 104B
Location: Blavatnik LT1
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 106B: FM Invited Talk: Leonardo de Moura
Location: Blavatnik LT1
09:00
Efficient verification and metaprogramming in Lean (abstract)
10:00-10:30 Session 107
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 108B
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 108C
Location: Blavatnik LT2
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 111: FLoC Plenary Lecture: Byron Cook
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 112B
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 112C
Location: Blavatnik LT2
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).

Tuesday, July 17th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

09:00-10:30 Session 114B
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 114C: FM I-Day
Location: Blavatnik LT2
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
12:00-12:30 Session 117
Location: Blavatnik LT1
12:00
View abstraction for systems with component identities (abstract)
12:30-14:00Lunch Break
14:00-15:30 Session 118B
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 118C: FM I-Day
Location: Blavatnik LT2
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 119B
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 119C: FM I-Day
Location: Blavatnik LT2
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)