Skip to main content

AIMS Seminar - 24th January 2020 @ 10:00am in LR7

Automated, Sound and Scalable Analysis and Control of Dynamical Models with SAT and SMT

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.