Hosted at the University of York, Professor Jim Woodcock will discuss his work on the verification of artificial neural networks.
Watch the video
Download the presentation slides (PDF)
Synopsis
Verifying learning-enabled robotic systems is challenging. There are existing techniques and tools for verifying artificial neural networks (ANNs), but they are focused on component-level properties.
We verify robotic systems with ANN control components. Currently, we focus on trained, fully connected ReLU neural networks for control. We use RoboChart, a domain-specific robot modelling and verification framework.
In RoboChart, we combine behavioural and ANN models, and we combine traditional and ANN-specific verification tools: Isabelle/HOL and Marabou. We report on exploratory work. In future, we will address the training phase, other ANN classes, and more sophisticated activation functions.
We collaborate with Ziggy Attala, Ana Cavalcanti, and Matt Windsor in the RoboStar Centre and colleagues at the Chinese Academy of Sciences.
About the speaker
Jim Woodcock
Jim Woodcock attended the University of Liverpool, where he was awarded a BSc (hons) in Computational Science (1977), an MSc in Operational Mathematics (1978), and a PhD in Computation (1980). He worked at the GEC Hirst Research Centre from 1980 to 1984, where he rose from Research Scientist to Principal Research Scientist and GEC Research Fellow.
In 1984, he joined the Department of Electrical and Electronic Engineering at the University of Surrey as a Lecturer in Information Technology. In 1985, he moved to the Programming Research Group at the University of Oxford as a research assistant to work with Tony Hoare and Ib Holm Sørensen on a collaborative project with IBM Hursley formalising the CICS transaction priocessing system.
This won the Queen's Award for Technological Achievement in 1996. During this time, he was a Junior Research Fellow at Wolfson College (1985-87) and an Atlas Fellow at Pembroke College and at the Rutherford-Appleton Laboratory (1987-91). He was appointed as a Lecturer in Computation in 1994, promoted to a Readership in Software Engineering in 1997, and appointed to a personal chair in 2000. He has been a Fellow of Kellogg College in Oxford since 1994.
In 2001, he moved to the University of Kent and in 2004 he moved to the University of York, in both cases as Professor of Software Engineering. He has been head of the Department of Computer Science at York since 2012. He was appointed to a Fellowship of the Royal Academy of Engineering in 2011.
Our events are for adults aged 16 years and over.
BCS is a membership organisation. If you enjoy this event, please consider joining BCS. You’ll be very welcome. You’ll receive access to many exclusive career development tools, an introduction to a thriving professional community and also help us Make IT Good For Society. Join BCS today
For overseas delegates who wish to attend the event, please note that BCS does not issue invitation letters.
This event is brought to you by: FACS (Formal Aspects of Computing Science) group and RoboStar Centre, University of York
