Alessandro Abate Seminar

Abstract: As a concluding bit of the 'Modern Control’ module, I would like to discuss some recent work that utilises tools and techniques from formal methods (automated verification) to analyse dynamical models and to synthesise controllers. The focus will be on SAT and SMT tools, underpinned by the CEGIS paradigm, where: 

SAT = Boolean satisfiability;

SMT = SAT modulo theory; and

CEGIS = counter-example guided inductive synthesis.

The attractive features of these approaches are their automation, soundness, and scalability.