# Abstracts

## Contributed talks

PDF document## Invited talks

### David S. Johnson

*Bin Packing: From Theory to Experiment and Back Again*

In the bin packing problem, one is given a list of 1-dimensional items
and asked to pack them into a minimum number of unit-capacity bins.
This was one of the first NP-hard problems to be studied from
the "approximation algorithm" point of view, and over the years
it has served as a laboratory for the study of new questions about
approximation algorithms and the development of new techniques
for their analysis. In this talk I present a brief survey of this
history, highlighting the many surprising average case behavior results
that have been obtained. Several of these surprises were first
revealed by experimentation, which led to conjectures and then
to proofs, and I will describe this interplay between experimentation
and theory. I'll also highlight some as-yet-unproven conjectures
suggested by the experimental data.
### Cliff Jones

*AI4FM - how to say "why" in proofs*

The AI4FM project is exploring how to use AI thinking in discharging
proof obligations (POs) that arise in the formal development of
programs. Of course, developing better and better heuristics for
theorem provers has been explored by AI researchers since its early
days. The approach being taken in this project (with Alan Bundy
providing the main AI input) is to design a system that can learn from
how an expert tackles POs that are beyond current heuristics. We have
industrial data that suggests as few as 5 ideas might kill off a
hundred undischarged POs. The first step is to design ways of
recording the insights which are often about "why" the expert chose a
strategy; we will move on to learning such strategies in the next
phase of the AI4FM project.
### Carsten Witt

*Bio-Inspired Computation Meets Theoretical Computer Science*

Biologically inspired methods of computation such as evolutionary
algorithms, ant colony optimisation, particle swarm optimisation
etc. are well established in numerous engineering disciplines. As
their computational complexity was generally unknown, these approaches
lived in the shadows of theoretical computer science for a long
time. This dramatically changed in recent years, when bio-inspired
computation was finally perceived as a family of algorithms and
analysed using methods from classical algorithms and complexity
theory.This talk will present some of the most exciting results that have been obtained in this new research area. We focus on evolutionary algorithms and ant colony optimisation in combinatorial optimisation and prove how they efficiently find optimal or approximate solutions to problems known from the theory of algorithms.