Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • External authors:
  • Alessandro Abate
  • Iury Bessa
  • Dario Cattaruzza
  • Cristina David
  • Pascal Kesseli
  • Daniel Kroening


Modern control is implemented with digital microcontrollers, embedded within a dynamical plant that represents physical components. We present a new algorithm based on counterexample guided inductive synthesis that automates the design of digital controllers that are correct by construction. The synthesis result is sound with respect to the complete range of approximations, including time discretization, quantization effects, and finite-precision arithmetic and its rounding errors. We have implemented our new algorithm in a tool called DSSynth, and are able to automatically generate stable controllers for a set of intricate plant models taken from the literature within minutes.

Bibliographical metadata

Original languageEnglish
Title of host publication20th ACM International Conference on Hybrid Systems: Computation and Control (HSCC)
Publication statusPublished - 2017
Eventthe 20th International Conference - Pittsburgh, Pennsylvania, USA
Event duration: 18 Apr 201720 Apr 2017


Conferencethe 20th International Conference

Related information


View all