A General Verification Framework for Dynamical and Control Models via
  Certificate Synthesis
Alec Edwards Andrea Peruffo Alessandro Abate
An emerging branch of control theory specialises in certificate learning,
concerning the specification of a desired (possibly complex) system behaviour
for an autonomous or control model, which is then analytically verified by
means of a function-based proof. However, the synthesis of controllers abiding
by these complex requirements is in general a non-trivial task and may elude
the most expert control engineers. This results in a need for automatic
techniques that are able to design controllers and to analyse a wide range of
elaborate specifications. In this paper, we provide a general framework to
encode system specifications and define corresponding certificates, and we
present an automated approach to formally synthesise controllers and
certificates. Our approach contributes to the broad field of safe learning for
control, exploiting the flexibility of neural networks to provide candidate
control and certificate functions, whilst using SMT-solvers to offer a formal
guarantee of correctness. We test our framework by developing a prototype
software tool, and assess its efficacy at verification via control and
certificate synthesis over a large and varied suite of benchmarks.