CAV Program

16:30	Tom Melham Proof Scripting from HOL to Goaled (abstract)
17:00	Michael Norrish HOL Developed and HOL Used: Interconnected Stories of Real-World Applications (abstract)
17:30	Magnus Myreen 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 abstracts session overview talk overview side by side with other conferences

09:00-10:30 Session 93A: FLoC Keynote Lecture: Georges Gonthier

Chair:

Assia Mahboubi

Location: Maths LT1

09:00

Georges Gonthier

The Logic of Real Proofs (abstract)

10:30-11:00Coffee Break

11:00-12:30 Session 95A: Model Checking

Chair:

Kedar Namjoshi

Location: Maths LT1

11:00	Yuki Satake and Hiroshi Unno Propositional Dynamic Logic for Higher-Order Functional Programs (abstract)
11:15	Grigory Fedyukovich, Yueling Zhang and Aarti Gupta Syntax-Guided Termination Analysis (abstract)
11:30	Hazem Torfah, Bernd Finkbeiner and Christopher Hahn Model Checking Quantitative Hyperproperties (abstract)
11:45	Lauren Pick, Grigory Fedyukovich and Aarti Gupta Exploiting Synchrony and Symmetry in Relational Verification (abstract)
12:00	Lucas Cordeiro, Pascal Kesseli, Daniel Kroening, Peter Schrammel and Marek Trtik JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (abstract)
12:15	Kenneth McMillan 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

Eran Yahav

From Programs to interpretable Deep Models, and Back (abstract)

15:00-15:30 Session 98A: Polyhedra

Chair:

Arie Gurfinkel

Location: Maths LT1

15:00	Gagandeep Singh, Markus Püschel and Martin Vechev Fast Numerical Program Analysis with Reinforcement Learning (abstract)
15:15	Anna Becchi and Enea Zaffanella A Direct Encoding for NNC Polyhedra (abstract)

15:30-16:00Coffee Break

16:00-18:00 Session 99A: Synthesis

Chair:

Barbara Jobstmann

Location: Maths LT1

16:00	S. Akshay, Supratik Chakraborty, Shubham Goel, Sumith Kulal and Shetal Shah What’s hard about Boolean Functional Synthesis? (abstract)
16:15	Alessandro Abate, Cristina David, Pascal Kesseli, Kroening Daniel and Elizabeth Polgreen Synthesis Modulo Theories (abstract)
16:30	Bernd Finkbeiner, Leander Tentrup, Marvin Stenger, Philip Lukert and Christopher Hahn Synthesizing Reactive Systems from Hyperproperties (abstract)
16:45	Daniel J. Fremont and Sanjit A. Seshia Reactive Control Improvisation (abstract)
17:00	Aws Albarghouthi and Justin Hsu Constraint-Based Synthesis of Coupling Proofs (abstract)
17:15	Chuchu Fan, Umang Mathur, Sayan Mitra and Mahesh Viswanathan Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics (abstract)
17:30	Suguman Bansal, Kedar Namjoshi and Yaniv Sa'Ar Synthesis Of Asynchronous Reactive Programs From Temporal Specifications (abstract)
17:45	Qinheping Hu and Loris D'Antoni 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).

Location: Oxford Town Hall

Sunday, July 15th

View this program: with abstracts session overview talk overview side by side with other conferences

09:00-10:00 Session 101A: CAV Award

Location: Maths LT1

10:00-10:30 Session 102A: Learning

Chair:

Ezio Bartocci

Location: Maths LT1

10:00	Xinyu Wang, Greg Anderson, Isil Dillig and Ken McMillan Learning Abstractions for Program Synthesis (abstract)
10:15	George Argyros and Loris D'Antoni The Learnability of Symbolic Automata (abstract)

10:30-11:00Coffee Break

11:00-12:30 Session 103A: Runtime Verification, Hybrid and Timed Systems

Chair:

Stefan Kiefer

Location: Maths LT1

11:00	Hui Kong, Ezio Bartocci and Tom Henzinger Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes (abstract)
11:15	Goran Frehse, Mirco Giacobbe and Thomas Henzinger Spacetime Interpolants (abstract)
11:30	Michael Emmi and Constantin Enea Monitoring Weak Consistency (abstract)
11:45	Yijun Feng, Joost-Pieter Katoen, Haokun Li, Bican Xia and Naijun Zhan Monitoring CTMCs By Multi-Clock Timed Automata (abstract)
12:00	Frederik M. Bønneland, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marco Muñiz and Jiri Srba Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (abstract)
12:15	Ezio Bartocci, Roderick Bloem, Dejan Nickovic and Franz Roeck A Counting Semantics for Monitoring LTL Specifications over Finite Traces (abstract)

12:30-14:00Lunch Break

14:00-15:30 Session 105A: Tools

Chair:

Dirk Beyer

Location: Maths LT1

14:00	Jan Kretinsky, Tobias Meggendorfer and Salomon Sickert Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (abstract)
14:15	Philipp J. Meyer, Salomon Sickert and Michael Luttenberger Strix: Explicit Reactive Synthesis Strikes Back! (abstract)
14:30	Aina Niemetz, Mathias Preiner, Clifford Wolf and Armin Biere BTOR2, BtorMC and Boolector 3.0 (abstract)
14:45	Marco Eilers and Peter Müller Nagini: A Static Verifier for Python (abstract)
15:00	Michael Blondin, Javier Esparza and Stefan Jaax Peregrine: A Tool for the Analysis of Population Protocols (abstract)
15:15	Milan Ceska, Jiri Matyas, Vojtech Mrazek, Lukas Sekanina, Zdenek Vasicek and Tomas Vojnar ADAC: Automated Design of Approximate Circuits (abstract)

15:30-16:00Coffee Break

16:00-17:00 Session 107A: Probabilistic Systems

Chair:

Sanjit A. Seshia

Location: Maths LT1

16:00	Edon Kelmendi, Julia Krämer, Jan Kretinsky and Maximilian Weininger Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (abstract)
16:15	Tim Quatmann and Joost-Pieter Katoen Sound Value Iteration (abstract)
16:30	Weichao Zhou and Wenchao Li Safety-Aware Apprenticeship Learning (abstract)
16:45	Qiyi Tang and Franck van Breugel Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains (abstract)

17:00-18:00 Session 108: Business Meeting

Location: Maths LT1

Monday, July 16th

View this program: with abstracts session overview talk overview side by side with other conferences

09:00-10:30 Session 109A: Tools

Chair:

Clark Barrett

Location: Maths LT1

09:00	Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja and Thomas Noll Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs (abstract)
09:15	Mostafa Hassan, Caterina Urban, Marco Eilers and Peter Müller MaxSMT-Based Type Inference for Python 3 (abstract)
09:30	Andrew Gacek, John Backes, Michael Whalen, Lucas Wagner and Elaheh Ghassabani The JKind Model Checker (abstract)
09:45	Vincent Cheval, Steve Kremer and Itsaka Rakotonirina The DEEPSEC prover (abstract)
10:00	Jianwen Li, Rohit Dureja, Geguang Pu, Kristin Yvonne Rozier and Moshe Vardi SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability (abstract)
10:15	Dmitry Blotsky, Federico Mora, Murphy Berzish, Yunhui Zheng, Ifaz Kabir and Vijay Ganesh StringFuzz: A Fuzzer for String Solvers (abstract)

10:30-11:00Coffee Break

11:00-12:00 Session 111A: CAV Invited Talk: Somesh Jha

Location: Maths LT1

11:00

Somesh Jha

Semantic Adversarial Deep Learning (abstract)

12:00-12:30 Session 113: Static Analysis

Chair:

Thomas Wies

Location: Maths LT1

12:00	Jérôme Dohrau, Alexander J Summers, Caterina Urban, Severin Münger and Peter Müller Permission Inference for Array Programs (abstract)
12:15	Patrick Cousot, Roberto Giacobazzi and Francesco Ranzato 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

Chair:

Daniel Kroening

Location: Maths LT1

14:00

Byron Cook

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).

Location: Ashmolean Museum

Tuesday, July 17th

View this program: with abstracts session overview talk overview side by side with other conferences

09:00-10:30 Session 117A: Theory and Security

Chair:

Roderick Bloem

Location: Maths LT1

09:00	Suguman Bansal, Swarat Chaudhuri and Moshe Vardi Automata vs Linear-Programming Discounted-Sum Inclusion (abstract)
09:15	Matthew Bauer, Rohit Chadha, Mahesh Viswanathan and Prasad Sistla Model checking indistinguishability of randomized security protocols (abstract)
09:30	Weikun Yang, Pramod Subramanyan, Yakir Vizel, Aarti Gupta and Sharad Malik Lazy Self-Composition for Security Verification (abstract)
09:45	Jun Zhang, Pengfei Gao, Fu Song and Chao Wang SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks (abstract)
10:00	Krishnendu Chatterjee, Monika Henzinger, Veronika Loitzenbauer, Simin Oraee and Viktor Toman Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives (abstract)
10:15	Tom van Dijk Attracting Tangles to Solve Parity Games (abstract)

10:30-11:00Coffee Break

11:00-12:15 Session 119A: SAT, SMT and Decision Procedures

Chair:

Alexander Nadel

Location: Maths LT1

11:00	Soonho Kong, Armando Solar-Lezama and Sicun Gao Delta-Decision Procedures for Exists-Forall Problems over the Reals (abstract)
11:15	Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett and Cesare Tinelli Solving Quantified Bit-Vectors using Invertibility Conditions (abstract)
11:30	Markus N. Rabe, Leander Tentrup, Cameron Rasmussen and Sanjit A. Seshia Understanding and Extending Incremental Determinization for 2QBF (abstract)
11:45	Robert Robere, Antonina Kolokolova and Vijay Ganesh The Proof Complexity of SMT Solvers (abstract)
12:00	Benjamin Farinier, Sebastien Bardin, Richard Bonichon and Marie-Laure Potet Model Generation for Quantified Formulas: A Taint-Based Approach (abstract)

12:30-14:00Lunch Break

14:00-15:15 Session 121A: Concurrency

Chair:

Thomas Wahl

Location: Maths LT1

14:00	Xinhao Yuan, Junfeng Yang and Ronghui Gu Partial Order Aware Concurrency Sampling (abstract)
14:15	Suha Orhun Mutluergil, Constantin Enea, Ahmed Bouajjani and Serdar Tasiran Reasoning About TSO Programs Using Reduction and Abstraction (abstract)
14:30	Huyen T.T. Nguyen, Cesar Rodriguez, Marcelo Sousa, Camille Coti and Laure Petrucci Quasi-Optimal Partial Order Reduction (abstract)
14:45	Ahmed Bouajjani, Constantin Enea, Kailiang Ji and Shaz Qadeer On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony (abstract)
15:00	Elvira Albert, Miguel Gomez-Zamalloa, Miguel Isabel and Albert Rubio Constrained Dynamic Partial Order Reduction (abstract)

15:30-16:00Coffee Break

16:00-17:45 Session 122A: CPS, Hardware, Industrial Applications

Chair:

Tomas Vojnar

Location: Maths LT1

16:00	Mark Tullsen, Lee Pike, Nathan Collins and Aaron Tomb Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (abstract)
16:15	Andrey Chudnov, Nathan Collins, Byron Cook, Josiah Dodds, Brian Huffman, Colm MacCarthaigh, Stephen Magill, Eric Mertens, Eric Mullen, Serdar Tasiran, Aaron Tomb and Edwin Westbrook Continuous formal verification of Amazon s2n (abstract)
16:30	Daniel Schemmel, Julian Büning, Oscar Soria Dustmann, Thomas Noll and Klaus Wehrle Symbolic Liveness Analysis of Real-World Software (abstract)
16:45	Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig and Mark R. Tuttle Model Checking Boot Code from AWS Data Centers (abstract)
17:00	Taolue Chen, Jinlong He, Fu Song, Guozhen Wang, Zhilin Wu and Jun Yan Android Stack Systems (abstract)
17:15	Christoph Walther Formally Verified Montgomery Multiplication (abstract)
17:30	Eric Goubault, Sylvie Putot and Lorenz Sahlman Inner and Outer Approximating Flowpipes for Delay Differential Equations (abstract)