Ben Batten joined the group this October as a PhD student. We caught up with him to find out about his previous research and what he does in his spare time.

So Ben, tell us a bit about where you’re from.

I grew up in a small town on the south coast called Lymington. My early life was dominated by sailing and I still love to sail – when I was at Bath University I was captain of their sailing club. We trained at Chew Valley lake nearby and took part in team racing events against other university clubs. I hope to join Imperial’s sailing club when it re-opens, but we did beat them when I was at Bath so I’m not sure how popular I’ll be!

What were you studying in Bath?

I studied for a BSc and MSc in physics. My Master’s dissertation explored the Leidenfrost effect, a phenomenon that occurs when a liquid droplet touches a heat surface that is hotter than the liquid’s boiling point: some of the edge of the droplet creates a layer of vapour between the droplet and the heat surface, and this stops it evaporating immediately. You can see this when you sprinkle water into a hot frying pan: the water droplets jump around the pan on a cushion of vapour instead of evaporating. This phenomenon can be exploited to make droplets propel along a surface, and using a ratchet-type mechanism, even travel uphill. My project explored how surface structures can aid this propulsion. This technology could be used in the engraving of the surface of computer components to carry heat away.

That sounds quite different to the work in the SAIL (formerly VAS) group! So how did you become interested in verification systems?

My project required lots of computer modelling, and extensive programming and coding. As I did more coding I became more interested in machine learning and reinforcement learning, and thought it would be really interesting to explore this more.

What will you be working on here?

My project will look at the formal verification of autonomous perception systems. This will require developing rigorous methods to identify weakness in autonomous systems, or in the absence of any weaknesses, to formally verify them. Many tools that have been developed so far are locally robust, which means they can only verify finite sub-sections within a system. We want to scale up these methods to look at global robustness of autonomous perception systems. The benefits are potentially huge, since without guarantees of robustness, this will hold back the widespread adoption of autonomous systems.