FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
CAV PROGRAM

Days: Friday, July 13th Saturday, July 14th Sunday, July 15th Monday, July 16th Tuesday, July 17th

Friday, July 13th

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

09:00-10:30 Session 83C: CAV Tutorial: Shaz Qadeer (part 1)
Location: Maths LT3
09:00
Proving a concurrent program correct by demonstrating it does nothing (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 86B: CAV Tutorial: Shaz Qadeer (part 2)
Location: Maths LT3
11:00
Proving a concurrent program correct by demonstrating it does nothing (continued) (abstract)
12:30-14:00Lunch Break
14:00-15:30 Session 87C: CAV Tutorial: Matteo Maffei
Location: Maths LT3
14:00
Foundations and Techniques for the Static Analysis of Ethereum Smart Contracts (abstract)
15:30-16:00Coffee Break
16:30-18:00 Session 90: Talks in memoriam Mike Gordon
Location: Maths LT3
16:30
Proof Scripting from HOL to Goaled (abstract)
17:00
HOL Developed and HOL Used: Interconnected Stories of Real-World Applications (abstract)
17:30
From Processor Verification Upwards (abstract)
19:00-21:30 Workshops dinner at Keble College

Workshops dinner at Keble College. Drinks reception from 7pm, to be seated by 7:30 (pre-booking via FLoC registration system required; guests welcome).

Location: Keble College
Saturday, July 14th

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

10:30-11:00Coffee Break
11:00-12:30 Session 95A: Model Checking
Location: Maths LT1
11:00
Propositional Dynamic Logic for Higher-Order Functional Programs (abstract)
11:15
Syntax-Guided Termination Analysis (abstract)
11:30
Model Checking Quantitative Hyperproperties (abstract)
11:45
Exploiting Synchrony and Symmetry in Relational Verification (abstract)
12:00
JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (abstract)
12:15
Eager Abstraction for Symbolic Model Checking (abstract)
12:30-14:00Lunch Break
14:00-15:00 Session 96A: CAV Invited Talk: Eran Yahav
Location: Maths LT1
14:00
From Programs to interpretable Deep Models, and Back (abstract)
15:00-15:30 Session 98A: Polyhedra
Location: Maths LT1
15:00
Fast Numerical Program Analysis with Reinforcement Learning (abstract)
15:15
A Direct Encoding for NNC Polyhedra (abstract)
15:30-16:00Coffee Break
16:00-18:00 Session 99A: Synthesis
Location: Maths LT1
16:00
What’s hard about Boolean Functional Synthesis? (abstract)
16:15
Synthesis Modulo Theories (abstract)
16:30
Synthesizing Reactive Systems from Hyperproperties (abstract)
16:45
Reactive Control Improvisation (abstract)
17:00
Constraint-Based Synthesis of Coupling Proofs (abstract)
17:15
Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics (abstract)
17:30
Synthesis Of Asynchronous Reactive Programs From Temporal Specifications (abstract)
17:45
Syntax Guided Synthesis with Quantitative Syntactic Objectives (abstract)
19:00-21:30 FLoC reception at Oxford Town Hall

FLoC reception at Oxford Town Hall. Drinks and canapés available from 7pm (pre-booking via FLoC registration system required; guests welcome).

Sunday, July 15th

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

10:00-10:30 Session 102A: Learning
Location: Maths LT1
10:00
Learning Abstractions for Program Synthesis (abstract)
10:15
The Learnability of Symbolic Automata (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 103A: Runtime Verification, Hybrid and Timed Systems
Location: Maths LT1
11:00
Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes (abstract)
11:15
Spacetime Interpolants (abstract)
11:30
Monitoring Weak Consistency (abstract)
11:45
Monitoring CTMCs By Multi-Clock Timed Automata (abstract)
12:00
Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (abstract)
12:15
A Counting Semantics for Monitoring LTL Specifications over Finite Traces (abstract)
12:30-14:00Lunch Break
14:00-15:30 Session 105A: Tools
Chair:
Location: Maths LT1
14:00
Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (abstract)
14:15
Strix: Explicit Reactive Synthesis Strikes Back! (abstract)
14:30
BTOR2, BtorMC and Boolector 3.0 (abstract)
14:45
Nagini: A Static Verifier for Python (abstract)
15:00
Peregrine: A Tool for the Analysis of Population Protocols (abstract)
15:15
ADAC: Automated Design of Approximate Circuits (abstract)
15:30-16:00Coffee Break
16:00-17:00 Session 107A: Probabilistic Systems
Location: Maths LT1
16:00
Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (abstract)
16:15
Sound Value Iteration (abstract)
16:30
Safety-Aware Apprenticeship Learning (abstract)
16:45
Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains (abstract)
Monday, July 16th

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

09:00-10:30 Session 109A: Tools
Location: Maths LT1
09:00
Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs (abstract)
09:15
MaxSMT-Based Type Inference for Python 3 (abstract)
09:30
The JKind Model Checker (abstract)
09:45
The DEEPSEC prover (abstract)
10:00
SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability (abstract)
10:15
StringFuzz: A Fuzzer for String Solvers (abstract)
10:30-11:00Coffee Break
12:00-12:30 Session 113: Static Analysis
Location: Maths LT1
12:00
Permission Inference for Array Programs (abstract)
12:15
Program Analysis is Harder than Verification: A Computability Perspective (abstract)
12:30-14:00Lunch Break
14:00-15:30 Session 114: 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 115A: 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
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 117A: Theory and Security
Location: Maths LT1
09:00
Automata vs Linear-Programming Discounted-Sum Inclusion (abstract)
09:15
Model checking indistinguishability of randomized security protocols (abstract)
09:30
Lazy Self-Composition for Security Verification (abstract)
09:45
SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks (abstract)
10:00
Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives (abstract)
10:15
Attracting Tangles to Solve Parity Games (abstract)
10:30-11:00Coffee Break
11:00-12:15 Session 119A: SAT, SMT and Decision Procedures
Location: Maths LT1
11:00
Delta-Decision Procedures for Exists-Forall Problems over the Reals (abstract)
11:15
Solving Quantified Bit-Vectors using Invertibility Conditions (abstract)
11:30
Understanding and Extending Incremental Determinization for 2QBF (abstract)
11:45
The Proof Complexity of SMT Solvers (abstract)
12:00
Model Generation for Quantified Formulas: A Taint-Based Approach (abstract)
12:30-14:00Lunch Break
14:00-15:15 Session 121A: Concurrency
Location: Maths LT1
14:00
Partial Order Aware Concurrency Sampling (abstract)
14:15
Reasoning About TSO Programs Using Reduction and Abstraction (abstract)
14:30
Quasi-Optimal Partial Order Reduction (abstract)
14:45
On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony (abstract)
15:00
Constrained Dynamic Partial Order Reduction (abstract)
15:30-16:00Coffee Break
16:00-17:45 Session 122A: CPS, Hardware, Industrial Applications
Location: Maths LT1
16:00
Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (abstract)
16:15
Continuous formal verification of Amazon s2n (abstract)
16:30
Symbolic Liveness Analysis of Real-World Software (abstract)
16:45
Model Checking Boot Code from AWS Data Centers (abstract)
17:00
Android Stack Systems (abstract)
17:15
Formally Verified Montgomery Multiplication (abstract)
17:30
Inner and Outer Approximating Flowpipes for Delay Differential Equations (abstract)