Days: Friday, July 13th Saturday, July 14th Sunday, July 15th Monday, July 16th Tuesday, July 17th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
| 09:00 | Proving a concurrent program correct by demonstrating it does nothing (abstract)  |
| 11:00 | Proving a concurrent program correct by demonstrating it does nothing (continued) (abstract) |
| 14:00 | Foundations and Techniques for the Static Analysis of Ethereum Smart Contracts (abstract) |
| 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) |
Workshops dinner at Keble College. Drinks reception from 7pm, to be seated by 7:30 (pre-booking via FLoC registration system required; guests welcome).
View this program: with abstractssession overviewtalk overviewside by side with other conferences
| 09:00 | The Logic of Real Proofs (abstract) |
| 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) |
| 14:00 | From Programs to interpretable Deep Models, and Back (abstract) |
| 15:00 | Fast Numerical Program Analysis with Reinforcement Learning (abstract) |
| 15:15 | A Direct Encoding for NNC Polyhedra (abstract) |
| 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) |
FLoC reception at Oxford Town Hall. Drinks and canapés available from 7pm (pre-booking via FLoC registration system required; guests welcome).
View this program: with abstractssession overviewtalk overviewside by side with other conferences
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.
| 10:00 | Learning Abstractions for Program Synthesis (abstract) |
| 10:15 | The Learnability of Symbolic Automata (abstract) |
| 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) |
| 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) |
| 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) |
View this program: with abstractssession overviewtalk overviewside by side with other conferences
| 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) |
| 11:00 | Semantic Adversarial Deep Learning (abstract) |
| 12:00 | Permission Inference for Array Programs (abstract) |
| 12:15 | Program Analysis is Harder than Verification: A Computability Perspective (abstract)  |
| 14:00 | Formal Reasoning about the Security of Amazon Web Services (abstract) |
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.
FLoC banquet at Ashmolean Museum. Drinks and food available from 7pm (pre-booking via FLoC registration system required; guests welcome).
View this program: with abstractssession overviewtalk overviewside by side with other conferences
| 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) |
| 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) |
| 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) |
| 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) |