Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants

Alessandro Abate, Lury Bessa, Dario Cattaruzza, Lucas Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

22 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationHSCC '17: Proceedings of the 20th International Conference on Hybrid Systems
Subtitle of host publicationComputation and Control
PublisherAssociation for Computing Machinery (ACM)
Number of pages10
Publication statusPublished - 18 Apr 2017
EventACM International Conference on Hybrid Systems: Computation and Control - Pittsburgh, United States
Duration: 18 Apr 201720 Apr 2017
Conference number: 20


ConferenceACM International Conference on Hybrid Systems
Abbreviated titleHSCC 2017
CountryUnited States
Internet address

Structured keywords

  • Programming Languages

Fingerprint Dive into the research topics of 'Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants'. Together they form a unique fingerprint.

Cite this