Facebook London has built a great team to bring the latest bugfinding techniques into Facebook’s development process. A lot of the time, they are having to develop those techniques themselves. But, they also give grants to academic groups to encourage them and they hold an annual two day symposium to talk about the challenges, progress, techniques, etc. The symposium was open to anybody interested in the topic: I met Facebook staff, many academic researchers (professors and PhD students), people from some of the other major tech companies, people from automative industry, entrepreneurs creating bugfinding tools, and many others. I think it is great that Facebook is investing in developing the testing and verification community in this way.

Most symposia have two components: time listening to prepared talks; and time spent networking over coffee/food in the breaks. This symposium also encouraged speakers and the audience to ask lots of questions during talks; they said that the audience’s job was to prevent the speaker from getting to their final slide and, in some cases we managed to do that!

The talks covered a range of test-related topics including:

• Re-evaluating different approaches to using ML to detect malicious code in Android. (This also touched on issues of (non)-reproducibility of published results.)

• Probabilistic Model Checking and Program synthesis. These two talks were the main ones that focussed on formal verification.

• A great (and funny) talk about fuzz testing, with a focus around grammar based testing, extracting grammars, etc. One of the questions lead to the response that fuzz testing is really trace generation and you need to add something else to turn it into a test. I also learned about this online book about fuzz testing about including Jupyter notebooks for experimenting with the code.

• Testing GUI-based systems.

• Peter O’Hearn talked about his “Incorrectness Logic” – I am looking forward to reading the full paper about this.

• Testing data (e.g., map data)

• Using ML to learn how simple bugs get fixed and then automatically submitting the fixes for review.

• Mike Papadakis presented a survey of mutation based testing based on his joint paper on the topic.

• Sir Tony Hoare ended the symposium with his perspectives on the field of testing and formal verification.

One of the fun things about having CAR Hoare in the audience is recognising all the times that people build on the work he did 40-50 years ago and wondering how often the speaker even realizes that they are doing so. Some things that were mentioned were Hoare Logic (of course), quicksort and null pointers.

These days, my verification work mostly involves using formal verification tools so many of the talks were teaching me new things and during some of the talks, I found myself wondering if the same techniques could be adapted for use with formal verification.