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 51C: CAV Tutorial: Shaz Qadeer (part 1)
09:00
Proving a concurrent program correct by demonstrating it does nothing ( abstract )
10:30-11:00Coffee Break
11:00-12:30 Session 54B: CAV Tutorial: Shaz Qadeer (part 2)
11:00
Proving a concurrent program correct by demonstrating it does nothing (continued) ( abstract )
12:30-14:00Lunch Break
14:00-15:30 Session 55C: CAV Tutorial: Matteo Maffei
14:00
Foundations and Techniques for the Static Analysis of Ethereum Smart Contracts ( abstract )
15:30-16:00Coffee Break
16:30-18:00 Session 58: Talks in memoriam Mike Gordon
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 Session : 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).

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 63A: Model Checking
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 64A: CAV Invited Talk: Eran Yahav
14:00
From Programs to interpretable Deep Models, and Back ( abstract )
15:00-15:30 Session 66A: Polyhedra
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 67A: Synthesis
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 Session : 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 70A: Learning
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 71A: Runtime Verification, Hybrid and Timed Systems
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 73A: Tools
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 75A: Probabilistic Systems
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 76A: Tools
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 80: Static Analysis
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 81: FLoC Plenary Lecture: Byron Cook
14:00
Formal Reasoning about the Security of Amazon Web Services ( abstract )
15:30-16:00Coffee Break
19:00-21:30 Session : 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 84A: Theory and Security
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 86A: SAT, SMT and Decision Procedures
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 88A: Concurrency
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 89A: CPS, Hardware, Industrial Applications
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 )