Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants

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

Research output: Contribution to conferenceAbstractpeer-review


We present a sound and automated approach to synthesizing safe, digital controllers for physical plants represented as linear, time-invariant models. The synthesis accounts for errors caused by the digitization effects introduced by digital controllers operating in either fixed- or floating-point arithmetic. Our approach uses counterexample-guided inductive synthesis (CEGIS): in the first phase an inductive generalisation engine produces a possible solution that is safe for some possible initial conditions but may not be safe for all initial conditions. Safety for all initial conditions is then verified in a second phase either via bounded model checking or abstract acceleration; if the verification step fails, a counterexample is provided to the inductive generalisation and the process iterates until a safe controller is obtained. We implemented our approach in a tool named DSSynth (Digital-System Synthesizer) and demonstrate its practical value by automatically synthesizing safe controllers for physical plant models from the digital control literature.
Original languageEnglish
Number of pages2
Publication statusPublished - 18 May 2018
EventSeventh Workshop on Synthesis - Oxford, United Kingdom
Duration: 18 Jul 201818 Jul 2018


WorkshopSeventh Workshop on Synthesis
Abbreviated titleSYNT 2018
Country/TerritoryUnited Kingdom
Internet address


Dive into the research topics of 'Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants'. Together they form a unique fingerprint.

Cite this