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

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

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.

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 https://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).