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

09:10-10:00 Session 102: CAV Award

The CAV 2018 Award is given to: SAT-based and Bounded Model Checking

  • Armin Biere
  • Alessandro Cimatti
  • Edmund M. Clarke
  • Daniel Kroening
  • Flavio Lerda
  • Yunshan Zhu

Bounded Model Checking has revolutionized the way model checking is used and perceived. It has increased the capabilities of model checkers by orders of magnitude, turning them into a standard tool for hardware verification and a very important component of the toolkit available for software verification. BMC changed the focus of model checking from full verification to bug-finding.  The BMC problem is defined as follows: Given a bound k, is there an erroneous computation of the system of length k?  This problem is transformed to a Boolean formula that is satisfiable if and only if the system includes a computation of length k, which violates the specification. Focusing on the bounded problem enabled the authors to exploit the progress that was made in SAT solving around the same time, and simultaneously to bootstrap the tremendous progress in satisfiability solving that we have seen since. While early implementation of BMC focused on hardware, CBMC has demonstrated how it can be applied to realistic programs written in C. The ability to apply verification directly to C programs gave an enormous boost to a very large spectrum of applications in hardware and software industry and in academic research. The application areas include error explanation and localization, concurrent programs, equivalence checking, cyber-physical systems and control systems, test vector generation, worst-case execution time, security, and many other practical applications.

Location: Maths LT1
10:00-10:30 Session 103A: 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 104A: 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 106A: 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 108A: 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 110A: 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 114: 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 115: 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 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
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 118A: 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 120A: 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 122A: 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 123A: 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)