Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants

Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen

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

20 Citations (Scopus)
49 Downloads (Pure)


We present a sound and automated approach to synthesize safe digital feedback controllers for physical plants represented as linear, time-invariant models. Models are given as dynamical equations with inputs, evolving over a continuous state space and accounting for errors due to the digitization of signals by the controller. Our counterexample guided inductive synthesis (CEGIS) approach has two phases: We synthesize a static feedback controller that stabilizes the system but that may not be safe for all initial conditions. Safety is then verified either via BMC or abstract acceleration; if the verification step fails, a counterexample is provided to the synthesis engine and the process iterates until a safe controller is obtained. We demonstrate the practical value of this approach by automatically synthesizing safe controllers for intricate physical plant models from the digital control literature.
Original languageEnglish
Title of host publicationComputer Aided Verification
Subtitle of host publication29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I
EditorsRupak Majumdar, Viktor Kunčak
PublisherSpringer, Cham
ISBN (Electronic)9783319633879
ISBN (Print)9783319633862
Publication statusPublished - 13 Jul 2017
Event32nd IEEE/ACM International Conference on Automated Software Engineering - University of Illinois at Urbana-Champaign, Illinois, USA, Urbana-Champaign, Illinois, United States
Duration: 30 Oct 20173 Nov 2017
Conference number: 32

Publication series

NameLecture Notes in Computer Science
PublisherSpringer, Cham


Conference32nd IEEE/ACM International Conference on Automated Software Engineering
Abbreviated titleASE 2017
Country/TerritoryUnited States
CityUrbana-Champaign, Illinois
Internet address

Structured keywords

  • Programming Languages


Dive into the research topics of 'Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants'. Together they form a unique fingerprint.

Cite this