Abstract

I discuss the construction of sound proofs for the formal verification and control of complex stochastic models of dynamical systems and reactive programs. Neural proofs are made up of two parts. Proof rules encode requirements for the verification of general temporal specifications over the models of interest. Certificates are then constructed from said proof rules with an inductive approach, namely accessing samples from the dynamics and training neural nets, whilst generalising such networks via SAT-modulo-theory queries, based on the full knowledge of the models. In the context of sequential decision-making problems over stochastic models, I discuss how to additionally generate policies, strategies, and controllers, in order to formally attain given specifications.

About Alessandro Abate

Alessandro Abate is Professor of Verification and Control in the Department of Computer Science at the University of Oxford. Prior to this, he did research at Stanford University and at SRI International, and was an Assistant Professor at the Delft Center for Systems and Control at the Delft University of Technology. He received a Laurea degree from the University of Padua and his MSc and PhD from UC Berkeley. His research work spans logics, probability, and AI.

About Current Trends in Computer Science

This lecture is part of the Current Trends in Computer Science Lecture Series by the TU Wien Informatics Doctoral School, where renowned Guest Professors hold public lectures every semester. If you are studying with us, the lecture series can be credited as an elective course for students of master programs of computer science: 195.072 Current Trends in Computer Science. Additionally, you can join courses held by this year’s Guest Professors of our doctoral colleges and the TU Wien Informatics Doctoral School.

Curious about our other news? Subscribe to our news feed, calendar, or newsletter, or follow us on social media.