Sound and Automated Synthesis of Digital Stabilizing
Controllers for Continuous Plants
∗

Alessandro Abate1 , Iury Bessa2 , Dario Cattaruzza1 , Lucas Cordeiro1,2 ,
Cristina David1 , Pascal Kesseli1 and Daniel Kroening1

arXiv:1610.04761v3 [cs.SY] 16 Feb 2017

1

University of Oxford, Oxford, United Kingdom

ABSTRACT
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.

Keywords
Digital control synthesis, CEGIS, finite-word-length representation, time sampling, quantization

1.

INTRODUCTION

Modern implementations of embedded control systems
have proliferated with the availability of low-cost devices that
can perform highly non-trivial control tasks, with significant
impact in numerous application areas such as environmental
control and robotics [4, 17]. Correct control is non-trivial,
however. The problem is exacerbated by artifacts specific
to digital control, such as the effects of finite-precision arithmetic, time discretization, and quantization noise introduced
by A/D and D/A conversion. Thus, programming expertise
is a key barrier to broad adoption of correct digital controllers, and requires considerable knowledge outside of the
expertise of many control engineers.
Beyond classical a-posteriori validation in digital control,
there has been plenty of previous work aiming at verifying
a given designed controller, which however broadly lack automation. Recent work has studied the stability of digital
∗
Supported by EPSRC grant EP/J012564/1, ERC project
280053 (CPROVER) and the H2020 FET OPEN SC2 .

Permission to make digital or hard copies of all or part of this work for personal or
classroom use is granted without fee provided that copies are not made or distributed
for profit or commercial advantage and that copies bear this notice and the full citation
on the first page. Copyrights for components of this work owned by others than ACM
must be honored. Abstracting with credit is permitted. To copy otherwise, or republish,
to post on servers or to redistribute to lists, requires prior specific permission and/or a
fee. Request permissions from permissions@acm.org.
c 2017 ACM. ISBN .
DOI:

2

Federal University of Amazonas, Manaus, Brazil

controllers considering implementation aspects, i.e., fixedpoint arithmetic and the word length [8]. They exploit
advances in bit-accurate verification of C programs to obtain
a verifier for software-implemented digital control.
By contrast, we leverage a very recent step-change in the
automation and scalability of program synthesis. Program
synthesis engines use a specification as the starting point, and
subsequently generate a sequence of candidate programs from
a given template. The candidate programs are iteratively
refined to eventually satisfy the specification. Program synthesizers implementing Counter-Example Guided Inductive
Synthesis (CEGIS) [34] are now able to generate programs
for highly non-trivial specifications with a very high degree of
automation. Modern synthesis engines combine automated
testing, genetic algorithms, and SMT-based automated reasoning [1, 11].
By combining and applying state-of-the-art synthesis engines we present a tool that automatically generates digital
controllers for a given continuous plant model that are correct by construction. This approach delivers a high degree of
automation, promises to reduce the cost and time of development of digital control dramatically, and requires considerably less expertise than a-posteriori verification. Specifically,
we synthesize stable, software-implemented embedded controllers along with a model of a physical plant. Due to the
complexity of such closed-loop systems, in this work we focus
on linear models with known configurations, and perform
parametric synthesis of stabilizing digital controllers (further closed-loop performance requirements are left to future
work).
Our work addresses challenging aspects of the control synthesis problem. We perform digital control synthesis over a
hybrid model, where the plant exhibits continuous behavior
whereas the controller operates in discrete time and over a
quantized domain. Inspired by a classical approach [4], we
translate the problem into a single digital domain, i.e., we
model a digital equivalent of the continuous plant by evaluating the effects of the quantizers (A/D and D/A converters)
and of time discretization. We further account for uncertainties in the plant model. The resulting closed-loop system is
a program with a loop that operates on bit-vectors encoded
using fixed-point arithmetic with finite word length (FWL).
The three effects of 1. uncertainties, 2. FWL representation
and 3. quantization errors are incorporated into the model,
and are taken into account during the CEGIS-based synthesis
of the control software for the plant.
In summary, this paper makes the following original contributions.

• We automatically generate correct-by-construction digital controllers using an inductive synthesis approach.
Our application of program synthesis is non-trivial and
addresses challenges specific to control systems, such
as the effects of quantizers and FWL. In particular, we
have found that a two-stage verification engine that
continuously refines the precision of the fixed-point representation of the plant yields a speed-up of two orders
of magnitude over a conventional one-stage verification
engine.
• Experimental results show that DSSynth is able to efficiently synthesize stable controllers for a set of intricate
benchmarks taken from the literature: the median runtime for our benchmark set considering the faster engine
is 48 s, i.e., half of the controllers can be synthesized in
less than one minute.

2.
2.1

PRELIMINARIES
Discretization of the Plant

The digital controllers synthesized using the algorithm
we present in this paper are typically used in closed loops
with continuous (physical) plants. Thus, we consider continuous dynamics (the plant) and discrete parts (the digital
controller). In order to obtain an overall model for the synthesis, we discretize the continuous plant and particularly
look at the plant dynamics from the perspective of the digital
controller.
As we only consider transfer function models, and require
a z-domain transfer function G(z) that captures all aspects
of the continuous plant, which is naturally described via
a Laplace-domain transfer function G(s). The continuous
model of the plant must be discretized to obtain the corresponding coefficients of G(z).
Among the discretization methods in the literature [17],
we consider the sample-and-hold processes in complex systems [20]. On the other hand, the ZOH discretization models
the exact effect of sampling and DAC interpolation over the
plant.
Assumption 1. The sample-and-hold effects of the ADC
and the presence of the ZOH of the DAC are synchronized,
namely there is no delay between sampling the plant output
at the ADC and updating the DAC accordingly. The DAC
interpolator is an ideal ZOH.
Lemma 1. [4] Given a synchronized ZOH input and sampleand-hold output on the plant, with a sample time T satisfying
the Nyquist criterion, the discrete pulse transfer function
G(z, T ) is an exact z-domain representation of G(s), and can
be computed using the following formula:




G(s)
G(z, T ) = (1 − z −1 )Z L−1
.
(1)
s
t=kT
In this study, for the sake of brevity, we will use the notation G(z) to represent the pulse transfer function G(z, T ).
Lemma
1 ensures that the poles and zeros match under the

Z L−1 {·}t=kT operations, and it includes the ZOH dynamics in the (1 − z −1 ) term. This is sufficient for stability
studies over G(s) [15], i.e., if there is any unstable pole (in
the complex domain <{s} > 0), the pulse transfer function
in (1) will also present the same number of unstable poles
(|z| > 1) [17].

2.2

Model Imprecision, Finite Word Length
Representation and Quantization Effects

Let C(z) be a digital controller and G(z) be a discrete-time
representation of the plant, given as
C(z) =

β0 + β1 z −1 + ... + βMC z −MC
Cn (z)
=
,
Cd (z)
α0 + α1 z −1 + ... + αNC z −NC

(2)

G(z) =

b0 + b1 z −1 + ... + bMG z −MG
Gn (z)
=
.
Gd (z)
a0 + a1 z −1 + ... + aNG z −NG

(3)

~ and α
where β
~ are vectors containing the controller’s coefficients; similarly, ~b and ~a denote the plant’s coefficients; and
finally N(·) and M(·) indicate the order of the polynomials,
and we require in particular that NG ≥ MG .
Uncertainties in G(z) may appear owing to: 1. uncertainties in G(s) (we denote the uncertain continuous plant by
G (s)+∆ G (s)
Ĝ(s) = Gnd (s)+∆pp Gnd (s) to explicitly encompass the effects of
the uncertainty terms ∆p G(·) (s)) arising from tolerances/imprecision in the original model; 2. errors in the numerical
calculations due to FWL effects (e.g., coefficient truncation
and round-off, which will be denoted as ∆b Gn (s), ∆b Gd (s));
and 3. errors caused by quantization (which we model later
as as external disturbances ν1 and ν2 ). These uncertainties
are parametrically expressed by additive terms, eventually
resulting in an uncertain model Ĝ(z), such that:
Ĝ(z) =

Gn (z) + ∆Gn (z)
,
Gd (z) + ∆Gd (z)

(4)

which will be represented by the following transfer function:
Ĝ(z) =

b̂0 + b̂1 z −1 + ... + b̂MG z −MG
.
â0 + â1 z −1 + ... + âNG z −NG

(5)

Notice that, due to the nature of the methods we use for
the stability check, we require that the parametric errors
in the plant have the same polynomial order as the plant
itself (indeed, all other errors described in this paper fulfill this property). We also remark that, due to its native digital implementation, there are no parametric errors
(∆p Cn (z), ∆p Cd (z)) in the controller. Thus Ĉ(z) ≡ C(z).
We introduce next a notation based on the coefficients
of the polynomial to simplify the presentation. Let P N be
the space of polynomials of order N . Let P ∈ P M,N be a
rational polynomial PPnd , where Pn ∈ P M and Pd ∈ P N . For
a vector of coefficients
~ ∈ RN +M +2 = [n0 n1 . . . nM d0 d1 . . . dN ]T
P

(6)

and an uncertainty vector
~ ∈ RN +M +2 = [∆n0 . . . ∆nM ∆d0 . . . ∆dN ]T
∆P

(7)

we write
~
~ + ∆G,
~ where
Ĝ = G

(8)

~ ∈ RNG +MG +2 = [b0 . . . bM a0 . . . aN ]T ,
G
G
G
~ ∈ RNG +MG +2 = [∆b0 . . . ∆bM ∆a0 . . . ∆aN ]T .
∆G
G
G
In the following we will either manipulate the transfer functions G(z), C(z) directly, or work over their respective coef~ C
~ in vector form.
ficients G,
A typical digital control system with a continuous plant
and a discrete controller is illustrated in Figure 1. The DAC
and ADC converters introduce quantization errors (notice

ν2 (z)

ν1 (z)

DAC

ADC

Controller
R(z)

+

e(z)

Ĉ(z)

-

Plant

U (z)

+
+

U (s)

ZOH

Ŷ (s)

Ĝ(s)

Q2

+
+

Ŷ (z)

Q1

Figure 1: Closed-loop digital control system (cf. Section 2.2 for notation)

that each of them may have a different FWL representation
than the controller), which are modeled as disturbances ν1 (z)
and ν2 (z); G(s) is the continuous-time plant model with
parametric additive uncertainty ∆p Gn (s) and ∆p Gd (s) (as
mentioned above); R(z) is a given reference signal; U (z) is
the control signal; and Ŷ (z) is the output signal affected by
the disturbances and uncertainties in the closed-loop system
The ADC and DAC may be abstracted by transforming the
closed-loop system in Figure 1 into the digital system in
Figure 2, where the effect of ν1 and ν2 in the output Y (z) is
additive noise.
Controller
R(z)

+

e(z)
-

Ĉ(z)

U (z)

ν2 (z)
+
+

Plant
Ĝ(z)

where P n is the space of polynomials of n-th order, P n hI, F i
is the space of polynomials with coefficients in RhI, F i, and
(as a special case) F0 hI, F i(x) returns the element x̃ ∈ RhI, F i
that is closest to the real parameter x.
Similarly, Fn,m hI, F i(·) : P n,m → P n,m hI, F i applies the
same effect to a ratio of polynomials, where P n,m , P n,m hI, F i
are rational polynomial domains.
Thus, the perturbed controller model C̃(z) may be obn (z)
tained from the original model Ĉ(z) = C(z) = C
as
Cd (z)
follows:

ν1 (z)
+
+

Ŷ (z)

Figure 2: Fully digital equivalent to system in Figure 1
In Figure 2, two sources of uncertainty are illustrated:
parametric uncertainties model the errors (which are rep~ and uncertainties for the quantizations
resented by ∆p G),
in the ADC and DAC conversions (ν1 and ν2 ), which are
assumed to be non-deterministic. Recall that we discussed
how the quantization noise is an additive term, which means
it does not enter parametrically in the transfer function. Instead, we later show that the system is stable given these
non-deterministic disturbance.
The uncertain model may be rewritten as a vector of
~
~+
coefficients in the z-domain using equation (8) as Ĝ = G
~ The parametric uncertainties in the plant are assumed
∆p G.
to have the same order as the plant model, since errors of
higher order can move the closed-loop poles by large amounts,
thus preventing any given controller from stabilizing such a
setup. This is a reasonable assumption since most tolerances
do not change the architecture of the plant.

Direct use of controllers in fixed-point representation.
Since the controller is implemented using finite representation, C(z) also suffers disturbances from the FWL effects,
with roundoffs in coefficients that may change closed-loop
poles and zeros position, and consequently affect its stability,
as argued in [8].
Let Ĉ(z) be the digital controller transfer function represented using this FWL with integer size I and fractional
size F . The term I affects the range of the representation
and is set to avoid overflows, while F affects the precision
and the truncation after arithmetic operations. We shall
denote the FWL domain of the coefficients by RhI, F i and
define a function
Fn hI, F i(P ∈ P) : P n → P n hI, F i

~ = F hI, F i(c ),
~ ∧ c̃i ∈ P̃
, P̃ ∈ P n hI, F i : ci ∈ P
0
i

(9)

C̃(z) = FMC ,NC hI, F i(C(z)) =

FMC hI, F i(Ĉn (z))
FNC hI, F i(Ĉd (z))

. (10)

In the case of a digitally synthesized controller (as it is the
case in this work), C̃(z) ≡ Ĉ(z) ≡ C(z) because the synthesis
is performed directly using FWL representation. In other
words, we synthesize a controller that is already in the domain
RhI, F i and has therefore no uncertainties entering because
of FWL representations, that is, ∆b Cn (z) = ∆b Cd (z) = 0.

Fixed-point computation in program synthesis.
The program synthesis engine uses fixed-point arithmetic.
Specifically, we use the domain RhI, F i for the controller’s coefficients and the domain RhIp , Fp i for the plant’s coefficients,
where I and F , as well as Ip and Fp , denote the number of bits
for the integer and fractional parts, respectively, and where
it is practically motivated to consider RhIp , Fp i ⊇ RhI, F i.
Given the use of fixed-point arithmetic, we examine the
discretization effect during these operations. Let C̃(z) and
G̃(z) be transfer functions represented using fixed-point bitvectors.
C̃(z) =

β̃0 + β̃1 z −1 + ... + β̃MC z −MC
,
α̃0 + α̃1 z −1 + ... + α̃NC z −NC

(11)

G̃(z) =

b̃0 + b̃1 z −1 + ... + b̃MG z −MG
.
ã0 + ã1 z −1 + ... + ãNG z −NG

(12)

Recall that since the controller is synthesized in the RhI, F i
domain, C̃(z) ≡ Ĉ(z) ≡ C(z). However, given a real plant
Ĝ(z), we need to introduce G̃(z) = FMG ,NG hIp , Fp i(Ĝ(z)),
where
(b̂0 + ∆b b̂0 ) + ... + (b̂MG + ∆b b̂MG )z −MG
(â0 + ∆b â0 ) + ... + (âNG + ∆b âNG )z −NG
~
~
~ =G
~ + ∆p G
~ + ∆b G,
~
G̃ = Ĝ + ∆b G
(13)

G̃(z) =

where ∆b ci = c̃i − ĉi , and ∆b G represents the plant uncertainty caused by the rounding off effect. We capture the
~ = ∆p G
~ + ∆b G.
~
global uncertainty as ∆G

2.3

Closed-Loop Stability Verification under
Parametric Uncertainties, FWL Representation and Quantization Noise

Sound synthesis of the digital controller requires the consideration of the effect of FWL on the controller, and of
quantization disturbances in the closed-loop system. Let the
quantizer Q1 (ADC) be the source of a white noise ν1 , and
Q2 (DAC) be the source of a white noise ν2 . The following equation models the system in Figure 1, including the
~ and the FWL effects on the
parametric uncertainties ∆G
controller C̃(z):
Ŷ (z) = ν1 (z) + Ĝ(z)C̃(z)R(z) + Ĝ(z)ν2 (z) − Ĝ(z)C̃(z)Ŷ (z).
(14)
The above can be rewritten as follows:
Ŷ (z) = H1 (z)ν1 (z) + H2 (z)ν2 (z) + H3 (z)R(z),

(15)

where
H1 (z) =

1
,
1 + Ĝ(z)C̃(z)

H2 (z) =

Ĝ(z)
,
1 + Ĝ(z)C̃(z)

H3 (z) =

Ĝ(z)C̃(z)
.
1 + Ĝ(z)C̃(z)

Assumption 2. The quantization noises ν1 (from Q1)
and ν2 (from Q2) are uncorrelated white noises and their
amplitudes are always bounded by the half of quantization
step [4], i.e., |ν1 | ≤ q21 and |ν2 | ≤ q22 , where q1 and q2 are
the quantization steps of ADC and DAC, respectively.
A discrete-time dynamical system is said to be BoundedInput and Bounded-Output (BIBO) stable if bounded inputs
necessarily result in bounded outputs. This condition holds
true over an LTI model if and only if every pole of its transfer
function lies inside the unit circle [5]. Analyzing Eq. (15),
the following proposition provides conditions for the BIBO
stability of the system in Figure 1, with regards to the
exogenous signals R(z), ν1 , and ν2 , which are all bounded
(in particular, the bound on the quantization noise is given
by Assumption 2).
Proposition 1. [8, 15] Consider a feedback closed-loop
control system as given in Figure 1 with a FWL implementation of the digital controller C̃(z) = FMC ,NC hI, F i(C(z))
and uncertain discrete model of the plant from (6), (7)
Ĝ(z) =

Ĝn (z)
,
Ĝd (z)

~
~ + ∆p G.
~
Ĝ = G

Then Ĝ(z) is BIBO-stable if and only if:
• the roots of characteristic polynomial S(z) are inside
the open unit circle, where S(z) is:
S(z) = C̃n (z)Ĝn (z) + C̃d (z)Ĝd (z);

(16)

• the direct loop product C̃(z)Ĝ(z) has no pole-zero cancellation on or outside the unit circle.
Proposition 1 provides necessary (and sufficient) conditions for the controller to stabilize the closed-loop system,

~ quanconsidering plant parametric uncertainties (i.e., ∆p G),
tization noises (ν1 and ν2 ) and FWL effects in the control
software. In particular, note that the model for quantization
noise enters as a signal to be stabilized: in practice, if the
quantization noise is bounded, the noise may be disregarded
if the conditions on Proposition 1 are satisfied.
If the verification is performed using FWL arithmetic,
the above equations must use G̃(z) instead of Ĝ(z). The
former will provide sufficient conditions for the latter to be
stabilized.

3.
3.1

AUTOMATED PROGRAM SYNTHESIS
FOR DIGITAL CONTROL
Overview of the Synthesis Process

In order to synthesize closed-loop digital control systems,
we use a program synthesis engine. Our program synthesizer
implements Counter-Example Guided Inductive Synthesis
(CEGIS) [34]. We start by presenting its general architecture
followed by describing the parts specific to closed-loop control
systems. A high-level view of the synthesis process is given
in Figure 3. Steps 1 to 3 are performed by the user and
Steps A to D are automatically performed by our tool for
Digital Systems Synthesis, named DSSynth.
CEGIS-based control synthesis requires a formal verifier
to check whether a candidate controller meets the requirements when combined with the plant. We use the DigitalSystem Verifier (DSVerifier) [19] in the verification module
for DSSynth. It checks the stability of closed-loop control
systems and considers finite-word length (FWL) effects in the
digital controller, and uncertainty parameters in the plant
model (plant intervals) [8].
Given a plant model in ANSI-C syntax as input (Steps 1–3),
DSSynth constructs a non-deterministic model to represent
the plant family, i.e., it addresses plant variations as interval
sets (Step A), and formulates a function (Step B) using implementation details provided in Steps 2 and 3 to calculate
the controller parameters to be synthesized (Step C). Note
that DSSynth synthesizes the controller for the desired numerical representation and realization form. Finally, DSSynth
builds an intermediate ANSI-C code for the digital system
implementation, which is used as input for the CEGIS engine
(Step D).
This intermediate ANSI-C code model contains a specification φ for the property of interest (i.e., robust stability)
and is passed to the Counterexample-Guided Inductive Synthesis (CEGIS) module of CBMC [9], where the controller
is marked as the input variable to synthesize. CEGIS employs an iterative, counterexample-guided refinement process,
which is explained in detail in Section 3.2. CEGIS reports
a successful synthesis result if it generates a controller that
is safe with respect to φ. In particular, the ANSI-C code
model guarantees that a synthesized solution is complete
and sound with respect to the stability property φ, since
it does not depend on system inputs and outputs. In the
case of stability, the specification φ consists of a number of
assumptions on the polynomial coefficients, following Jury’s
Criteria, as well as the restrictions on the representation of
these coefficients as discussed in detail in Section 3.3.

3.2

Architecture of the Program Synthesizer

The input specification provided to the program synthesizer
~ .∀~
~ ) where P
~ ranges over functions,
is of the form ∃P
x.σ(~
x, P

User

Step 1
Determine plant
model and intervals

DSSynth

Step 2
Define controller
numerical representation

Step B
Formulate a FWL
effect function

Step A
Construct a nondeterministic plant model

Step 3
Define controller
realization form

Step C
Compute FWL
controller model

ANSI-C input
file

Intermediate
ANSI-C code

Step D
Synthesise digital
controller

Figure 3: Overview of the synthesis process

~
x ranges over ground terms and σ is a quantifier-free formula.
We interpret the ground terms over some finite domain D.
The design of our synthesizer is given in Figure 4 and
consists of two phases, Synthesize and Verify, which interact via a finite set of test vectors inputs that is updated
incrementally. Given the aforementioned specification σ,
~
the synth procedure tries to find an existential witness P
~
satisfying the specification σ(~
x, P ) for all ~
x in inputs (as
opposed to all ~x ∈ D). If synthesize succeeds in finding
~ , this witness is a candidate solution to the full
a witness P
synthesis formula. We pass this candidate solution to verify,
~ satisfies the
which checks whether it is a full solution (i.e., P
~
specification σ(~x, P ) for all ~
x ∈ D). If this is the case, then
the algorithm terminates. Otherwise, additional information
is provided to the synthesize phase in the form of a new
counterexample that is added to the inputs set and the loop
iterates again (the second feedback signal “Increase Precision” provided by the Verify phase in Figure 4 is specific to
control synthesis and will be described in the next section).
Each iteration of the loop adds a new input to the finite
set inputs that is used for synthesis. Given that the full set
of inputs D is finite, this means that the refinement loop can
only iterate a potentially very large, but finite number of
times.

3.3

Synthesis for Control

Formal specification of the stability property.
Next, we describe the specific property that we pass to
the program synthesizer as the specification σ. There are
a number of algorithms in our verification engine that can
be used for stability analysis [7, 8]. Here we choose Jury’s
criterion [4] in view of its efficiency and ease of integration
within DSSynth: we employ this method to check the stability
in the z-domain for the characteristic polynomial S(z) defined
in (16). We consider the following form for S(z):
S(z) = a0 z N + a1 z N −1 + · · · + aN −1 z + aN = 0, a0 6= 0.
Next, the following matrix M = [mij ](2N −2)×N is built
from S(z) coefficients:



M =


V (0)
V (1)
..
.




,


V (N −2)
(k)

where V (k) = [vij ]2×N such that:
(0)

vij =



aj−1 ,
if i = 1
0
v(1)(N
−j+1) , if i = 2

(k)

vij


0,
if j > n − k



(k−1)
(k−1)
(k−1) v11
−
v
.
v
,
if
j ≤ n − k and i = 1
=
(k−1)
2j
1j
v21


 vk
if j ≤ n − k and i = 2
(1)(N −j+1) ,

and where k ∈ Z is such that 0 < k < N −2. We have that [4]
S(z) is the characteristic polynomial of a stable system if
and only if the following four conditions hold: R1 : S(1) > 0;
R2 : (1)N S(1) > 0; R3 : |a0 | < aN ; R4 : m11 > 0 ∧ m31 > 0 ∧
m51 > 0 ∧ . . . ∧ m(2N −3)(1) > 0. The stability property
is then encoded by a constraint of the form: φstability ≡
(R1 ∧ R2 ∧ R3 ∧ R4 ).

The synthesis problem.
The synthesis problem we are trying to solve is the following: find a digital controller C̃(z) that makes the closed-loop
system stable for all possible uncertainties G̃(z) (13). When
mapping back to the notation used for describing the general
architecture of the program synthesizer, the controller C̃(z)
denotes P and G̃(z) represents x.
As mentioned above, we compute the coefficients for C̃(z)
in the domain RhI, F i, and those for G̃(z) in the domain
RhIp , Fp i. While the controller’s precision hI, F i is given, we
can vary hIp , Fp i such that RhIp , Fp i ⊇ RhI, F i. As the cost of
SAT solving increases with in the size of the problem instance,
our algorithm tries to solve the problem first for small Ip ,
Fp , iteratively increasing the precision if it is insufficient.

3.4

The Synthesize and Verify phases
The synthesize phase uses BMC to compute a solution
C̃(z). There are two alternatives for the verify phase. The
first approach uses interval arithmetic [28] to represent the
coefficients [ci − ∆p ci − ∆b ci , ci + ∆p ci − ∆b ci + (2−Fp )]
and rounds outwards. This0 allows us to simultaneously
evaluate the full collection of plants Ĝ(s) (i.e., all concrete
plants G(s) in the range G(s) ± ∆p G(s)) plus the effects of
numeric calculations. Synthesized controllers are stable for
all plants in the family. Preliminary experiments show that
a synthesis approach using this verification engine has poor
performance and we therefore designed a second approach.
Our experimental results in Section 4 show that the speedup
yielded by the second approach is in most cases of at least
two orders of magnitude.
The second approach is illustrated in Figure 4 and uses
a two-stage verification approach: the first stage performs
potentially unsound fixed-point operations assuming a plant
precision hIp , Fp i, and the second stage restores soundness
by validating these operations using interval arithmetic on
the synthesized controller. In more detail, in the first stage,
denoted by Uncertainty in Figure 4, assuming a precision
hIp , Fp i we check whether the system is unstable for the current candidate solution, i.e., if ¬φstability is satisfiable for S(z).
If this is the case, then we obtain a counterexample G̃(z),

Increase Precision
Verify

Candidate solution
Synthesize

Uncertainty
Counterexample
Candidate
UNSAT/
Inputs
P
model

UNSAT/
candidate

Closed-loop System Search

BMC-based Verifier

Precision

Done

Candidate
P

True/
False

Fixed-point Arithmetic Verifier

Figure 4: Counterexample-Guided Inductive Synthesis of Closed-loop Systems (Step D)

which makes the closed-loop system unstable. This uncertainty is added to the set inputs such that, in the subsequent
synthesize phase, we obtain a candidate solution consisting
of a controller C(z), which makes the closed-loop system
stable for all the uncertainties accumulated in inputs.
If the Uncertainty verification stage concludes that the
system is stable for the current candidate solution, then we
pass this solution to the second verification stage, Precision,
which checks the propagation of the error in the fixed-point
calculations using a Fixed-point Arithmetic Verifier based
on interval arithmetic.
If the precision verification returns false, then we increase
the precision of hIp , Fp i and re-start the synthesize phase
with an empty inputs set. Otherwise, we found a full sound
solution for our synthesis problem and we are done.
In the rest of the paper, we will refer to the two approaches
for the verify phase as one-stage and two-stage, respectively.

3.5

Soundness

The synthesise phase generates potentially unsound candidate solutions. The soundness of the model is ensured by
the verify phase. If a candidate solution passes verification,
it is necessarily sound.
The verify phase has two stages. The first stage ensures
that no counterexample plant with an unstable closed loop
exists over finite-precision arithmetic. Since the actual plant
uses reals, we need to ensure we do not miss a counterexample because of rounding errors. For this reason, the second
verification stage uses an overapproximation with interval
arithmetic with outward rounding. Thus, the first verification
stage underapproximates and is used to generate counterexamples, and the second stage overapproximates and provides
proof that no counterexample exists.

3.6

Illustrative Example

We illustrate our approach with a classical cruise control
example from the literature [5]. It highlights the challenges
that arise when using finite-precision arithmetic in digital
control. We are given a discrete plant model (with a time
step of 0.2 s), represented by the following z-expression:
G(z) =

0.0264
.
z − 0.9998

(17)

Using an optimization tool, the authors of [36] have designed a high-performance controller for this plant, which is
characterized by the following z-domain transfer function:
C(z) =

2.72z 2 − 4.153z + 1.896
.
z 2 − 1.844z + 0.8496

(18)

The authors of [36] claim that the controller C(z) in (18)

stabilizes the closed-loop system for the discrete plant model
G(z) in (17). However, if the effects of finite-precision arithmetic are considered, then this closed-loop system becomes
unstable. For instance, an implementation of C(z) using
Rh4, 16i fixed-point numbers (i.e., 4 bits for the integer part
and 16 bits for the fractional part) can be modeled as:
2

−4.1529998779296875z+1.89599609375
C̃(z):= 2.7199859619140625z
.
z 2 −1.843994140625z+0.8495941162109375
(19)
The resulting system, where C̃(z) and G(z) are in the forward
path, is unstable. Notice that this is disregarding further
approximation effects on the plant caused by quantization in
the verifier (i.e., G̃(z)). Figure 5a gives the Bode diagram for
the digital controller represented in (18): as the phase margin
is negative, the controller is unstable when considering the
FWL effects.

3.7

Program Synthesis for the Example

We now demonstrate how our approach solves the synthesis problem for the example given in the previous section.
Assuming a precision of Ip = 16, Fp = 24, we start with
an a-priori candidate solution with all coefficients zero (the
controller performs FWL arithmetic, hence we use C̃(z)):
C̃(z) =

0z 2 +0z+0
.
0z 2 +0z+0

In the first verify stage, the uncertainty check finds the
following counterexample:
G̃(z) =

0.026506
.
1.000610z + 1.002838

We add this counterexample to inputs and initiate the synthesize phase, where we obtain the following candidate
solution:
C̃(z) =

12.402664z 2 −11.439667z+0.596756
.
4.003906z 2 −0.287949z+0.015625

This time, the uncertainty check does not find any counterexample and we pass the current candidate solution to
the precision verification stage. We obtain the result false,
meaning that the current precision is insufficient. Consequently, we increase our precision to Ip = 20, Fp = 28.
Since the previous counterexamples were obtained at lower
precision, we remove them from the set of counterexamples. Back in the synthesize phase, we re-start the process
with a candidate solution with all coefficients 0, as above.
Next, the uncertainty verification stage provides the first
counterexample at higher precision:
G̃(z) =

0.026314
.
0.999024z−1.004785

Bode Diagram
Gm = 16.7 dB (at 2.12 rad/s) , Pm = −57.2 deg (at 1.29 rad/s)

Magnitude (dB)

10
0
−10
−20

Phase (deg)

−30
−90
−180
−270
−360
−450
−1
10

0

10

1

10

2

10

Frequency (rad/s)

(a) Original controller [36]
Bode Diagram
Gm = 17.8 dB (at 15.7 rad/s) , Pm = Inf

Magnitude (dB)

0
−5
−10
−15
−20

Phase (deg)

−25
0
−45
−90
−135
−180
−225
−1
10

0

10

1

10

2

10

Frequency (rad/s)

(b) Controller synthesized by DSSynth

Figure 5: Bode diagram for original controller in [36] and
for newly synthesized closed-loop system

In the synthesize phase, we get a new candidate solution
that eliminates the new, higher precision counterexample:
C̃(z) =

11.035202z 2 +5.846100z+4.901855
.
1.097901z 2 +0.063110z+0.128357

This candidate solution is validated as the final solution
by both stages uncertainty and precision in the verify
phase. Figure 5 compares the Bode diagram using the digital
controller represented by Eq. (18) from [36] (Figure 5a) and
the final candidate solution from our synthesizer (Figure 5b).
The DSSynth final solution is stable since it presents an
infinite phase margin and a gain margin of 17.8 dB.
Figure 6 illustrates the step responses of the closed-loop
system with the original controller represented by Eq. (18)
(Figure 6a), the first (Figure 6b) and final (Figure 6c) candidate solutions provided by DSSynth. The step response
in Figure 6a confirms the stability loss if we consider FWL
effects. Figure 6b shows that the first candidate controller is
able to stabilize the closed-loop system without uncertainties,
but it is rejected during the precision phase by DSSynth
since this solution is not sound. Finally, Figure 6c shows a
stable behavior for the final (sound) solution, which presents
a lower settling time (hence the digitization effects).

4.

EXPERIMENTAL EVALUATION

4.1

Description of the Benchmarks

The first set of benchmarks uses the discrete model G1 of
a cruise control system for a car, and accounts for rolling
friction, aerodynamic drag, and the gravitational disturbance
force [5]. The second set of benchmarks considers the discrete
model G2 of a simple spring-mass damper plant [36]. A third
set of benchmarks uses the discrete model G3 for satellite
attitude dynamics [17], which require attitude control for
orientation of antennas and sensors w.r.t. Earth. The fourth
set of benchmarks presents an alternative discrete model G4
of a cruise control system [36]. The fifth and sixth set of
benchmarks describe the discrete model of a DC servo motor
velocity dynamics [27, 35]. The seventh set of benchmarks
contains a well-studied discrete non-minimal phase model
G7 . Non-minimal phase models cause additional difficulties
for the design of stable controllers [12]. The eighth set of
benchmarks describes the discrete model G8 for the Helicopter Longitudinal Motion, which provides the longitudinal
motion dynamics of a helicopter [17]. The ninth set of benchmarks contains the discrete model G9 for the known Inverted
Pendulum, which describes a pendulum dynamics with its
center of mass above its pivot point [17]. The tenth set of
benchmarks contains the Magnetic Suspension discrete model
G10 , which describes the dynamics of a mass that levitates
with support only of a magnetic field [17]. The eleventh set
of benchmarks contains the Computer Tape Driver discrete
model G11 , which describes a system to read and write data
on a storage device [17]. The last set of benchmarks considers
a discrete model G12 that is typically used for evaluating
stability margins and controller fragility [23, 24].
Additional benchmarks were created for the Cruise Control
System, Spring-mass damper, and Satellite considering parametric additive in the nominal plant model (represented by
~ in Eq. (13)). The uncertainties are deviations bounded
∆p G
to a maximum magnitude of 0.5 in each coefficient. These
uncertain models are respectively represented by G1b , G2b ,
G3b and G3d .
All experiments have been conducted on a 12-core 2.40 GHz
Intel Xeon E5-2440 with 96 GB of RAM and Linux OS. All
times given are wall clock times in seconds, as measured
by the UNIX date command. For the two-stage verification
engine in Figure 4 we have applied a timeout of 8 hours per
benchmark, whereas 24 hours have been set for the approach
using a one-stage engine.

4.2

Objectives

Using the closed-loop control system benchmarks given in
Section 4.1, our experimental evaluation aims to answer two
research questions:
RQ1 (performance) does the CEGIS approach generate a
FWL digital controller in a reasonable amount of time?
RQ2 (sanity check) are the synthesized controllers sound
and can their stability be confirmed outside of our
model?

4.3

Results

We give the run-times required to synthesize a stable
controller for each benchmark in Table 1. Here, Plant is
the discrete or continuous plant model, Benchmark is the
name of the employed benchmark, I and F represent the

Step Response
Step Response

28

1.5

Step Response

x 10

1.4

1

1.2

0.9
1

0.8

1

0.5

0

Amplitude

Amplitude

Amplitude

0.7
0.6
0.5

0.8
0.6

0.4

0.4

0.3
−0.5

0.2

0.2
0.1
−1

0

50

100

150
200
Time (seconds)

250

(a) Original controller

300

350

0

0
0

50

100

150

0

0.5

Time (seconds)

(b) First solution by DSSynth

1

1.5
2
2.5
Time (seconds)

3

3.5

4

(c) Final solution by DSSynth

Figure 6: Step responses for original [36] closed-loop system with FWL effects and for each synthesize iteration of DSSynth
number of integer and fractional bits of the stable controller,
respectively, while the two right columns display the total
time (in seconds) required to synthesize a stable controller
for the given plant.
For the majority of the benchmarks, the conjecture explained in Section 3.3 holds and the two-stage verification
engine is able to find a stable solution in less than one minute
for half of the benchmarks. This is possible if the inductive
solutions need to be refined with few counterexamples and
increments of the fixed-point precision. However, the benchmark SatelliteB2 with uncertainty (G3b ) has required too
many counterexamples to refine its solution. For this particular case, the one-stage engine is able to complement the
two-stage approach and synthesizes a solution. It is important to reiterate that the one-stage verification engine does
not take advantage of the inductive conjecture inherent to
CEGIS, but instead fully explores the counterexample space
in a single SAT instance. As expected, this approach is significantly slower on average and is only useful for benchmarks
where the CEGIS approach requires too many refinement
iterations such that exploring all counterexamples in a single
SAT instance performs better. Our results suggest an average
performance difference of at least two orders of magnitude,
leading to the one-stage engine timing out on the majority
of our benchmarks. Table 1 lists the results for both engines,
where in 16 out of 23 benchmarks, the two-stage engine is
faster.
The presence of uncertainty in some particular benchmarks
(2, 4, 6, and 8) leads to harder verification conditions to be
checked by the verify phase, which impacts the overall
synthesis time. However, considering the faster engine for
each benchmark (marked in bold in Table 1), the median
run-time is 48 s, implying that DSSynth can synthesize half of
the controllers in less than one minute. Overall, the average
fastest synthesis time considering both engines is approximately 42 minutes. We consider these times short enough
to be of practical use to control engineers, and thus affirm
RQ1. We further observe that the two-stage verification
engine is able to synthesize stable controllers for 19 out of
the 23 benchmarks, and can be complemented using the onestage engine, which is faster for two benchmarks where the
inductive conjectures fail. Both verification engines together
enable controller synthesis for 20 out of 23 benchmarks. For
the remaining benchmarks our approach failed to synthesize a stable controller within the time limits. This can be
addressed by either increasing either the time limit or the
fixed-point word widths considered, or by using floating-point
arithmetic instead. The synthesized controllers have been

#
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

Plant
G1a
G1b
G2a
G2b
G3a
G3b
G3c
G3d
G4
G5
G6
G7
G8
G9
G10
G11
G12a
G12a
G12a
G12b
G12b
G12b
G12c

Benchmark
CruiseControl02
CruiseControl02†
SpgMsDamper
SpgMsDamper†
SatelliteB2
SatelliteB2†
SatelliteC2
SatelliteC2†
Cruise
DCMotor
DCServomotor
Doyleetal
Helicopter
Pendulum
Suspension
Tapedriver
a ST1 IMPL1
a ST1 IMPL2
a ST1 IMPL3
a ST2 IMPL1
a ST2 IMPL2
a ST2 IMPL3
a ST3 IMPL1

I
4
4
15
15
3
3
3
3
3
3
4
4
3
3
3
3
16
16
16
16
16
16
16

F
16
16
16
16
7
7
5
5
7
7
11
11
7
7
7
7
4
8
12
4
8
12
4

2-stage
12 s
14600 s
52 s
7
36 s
7
3s
50 s
1s
1s
46 s
8769 s
44 s
1s
1s
1s
11748 s
351 s
8772 s
1128 s
7
15183 s
7

1-stage
67 s
52 s
318 s
7
7
4111 s
205 s
1315 s
1s
10 s
7
7
7
14826 s
5s
1s
7
7
7
7
7
7
7

Table 1: DSSynth results (7 = time-out, † = uncertainty)

confirmed to be stable outside of our model representation
using MATLAB, positively answering RQ2. A link to the
full experimental environment, including scripts to reproduce
the results, all benchmarks and the DSSynth tool, is provided
in the footnote.1

4.4

Threats to Validity

We have reported a favorable assessment of DSSynth over
a diverse set of real-world benchmarks. Nevertheless, this
set of benchmarks is limited within the scope of this paper
and DSSynth’s performance needs to be assessed on a larger
benchmark set in future work.
Furthermore, our approach to select suitable FWL word
widths to model plant behavior employs a heuristic based
on user-provided controller word-width specifications. Given
the encouraging results of our benchmarks, this heuristic
appears to be strong enough for the current benchmark set,
but this may not generalize. Further experiments towards
determining suitable plant FWL configurations may thus be
necessary in future work.
Finally, the experimental results obtained using DSSynth
for stability properties may not generalize to other properties.
1

http://www.cprover.org/DSSynth/experiment.tar.gz
CBMC (SHA-1 hash) version:
7a6cec1dd0eb8843559591105235f1f2c4678801

The inductive nature of the two-stage back-end of DSSynth
increases performance significantly compared to the onestage back-end, but this performance benefit introduced
by CEGIS inductive generalizations may not be observed
for other controller properties. Additional experiments are
necessary to confirm that the performance of our inductive
synthesis approach can be leveraged in those scenarios.

5.

RELATED WORK

Robust Synthesis of Linear Systems.
The problem of parametric control synthesis based on stability measures for continuous Linear Time Invariant (LTI)
Single Input-Single Output (SISO) systems has been researched for several decades. On a theoretical level it is
a solved problem [37], for which researchers continuously
seek better results for a number of aspects in addition to
stability. A vast range of pole placement techniques such as
Moore’s algorithm for eigenstructure assignment [25] or the
more recent Linear Quadratic Regulator (LQR) [6] have been
used with increasing degrees of success. The latter approach
highlights the importance of conserving energy during the
control process, which results in lower running costs. Since
real systems are subject to tolerance and noise as well as
the need for economy, more recent studies focus on the problem of achieving robust stability with minimum gain [33,
26]. However, when applied with the aim of synthesizing a
digital controller, many of these techniques lack the ability
to produce sound or stable results because they disregard
the effects of quantization and rounding. Recent papers on
implementations/synthesis of LTI digital controllers [10, 18]
focus on time discretization, failing to account for these errorinducing effects and can result in digital systems that are
unstable even though they have been proven to be robustly
stable in a continuous space.

Formal Verification of Linear Digital Controllers.
Various effects of discretizing dynamics, including delayed
response [13] and Finite Word Length (FWL) semantics [3]
have been studied, with the goal to either verify [7] or to
optimize [29] given implementations.
There are two different problems that arise from FWL
semantics. The first is the error in the dynamics caused
by the inability to represent the exact state of the physical
system while the second relates to rounding errors during
computation. In [16], a stability measure based on the error
of the digital dynamics ensures that the deviation introduced
by FWL does not make the digital system unstable. A recent approach [38] uses the µ-calculus to directly model the
digital controller so that the selected parameters are stable
by design. Most work in verification focuses on finding a
correct variant of a known controller, looking for optimal
parameter representations using FWL, but ignore the effects
of rounding errors due to issues of mathematical tractability.
The analyses in [32, 36] rely on an invariant computation
on the discrete system dynamics using Semi-Definite Programming (SDP). While the former uses BIBO properties to
determine stability, the latter uses Lyapunov-based quadratic
invariants. In both cases, the SDP solver uses floating-point
arithmetic and soundness is checked by bounding the error.
An alternative approach is taken by [30], where the verification of existing code is performed against a known model
by extracting an LTI model of the code through symbolic

execution. In order to account for rounding errors, an upper
bound is introduced in the verification phase. If the error of
the implementation is lower than this tolerance level, then
the verification is successful.

Robust Synthesis of FWL Digital Controllers.
There is no technique in the existing literature for automatic synthesis of fixed-point digital controllers that considers FWL effects.
Other tools such as [14] are aimed at robust stability
problems, but they fail to take the FWL effects into account.
In order to provide a correct-by-design digital controller, [2]
requires a user-defined finite-state abstraction to synthesize
a digital controller based on high-level specifications. While
this approach overcomes the challenges presented by the
FWL problem, it still requires error-prone user intervention.
A different solution that uses FWL as the starting point is
an approach that synthesizes word lengths for known control
problems [22]; however, this provides neither an optimal
result nor a comprehensive solution for the problem.

The CEGIS Architecture.
Program synthesis is the problem of computing correctby-design programs from high-level specifications, and algorithms for this problem have made substantial progress in
recent years. One such approach [21] inductively synthesizes
invariants to generate the desired programs.
Program synthesizers are an ideal fit for synthesis of parametric controllers since the semantics of programs capture
effects such as FWL precisely. In [31], the authors use
CEGIS for the synthesis of switching controllers for stabilizing continuous-time plants with polynomial dynamics. The
work extends to its application on affine systems, finding its
major challenge in the hardness of solving linear arithmetic
with the state-of-the-art SMT solvers. Since this approach
uses switching states instead of linear dynamics in the digital
controller, it entirely circumvents the FWL problem. It is
also not suitable for the kind of control we seek to synthesize.
We require a combination of a synthesis engine with a control
verification tool that addresses the challenges presented here
in the form of FWL effects and stability measures for LTI
SISO controllers. We take the former from [11] and the latter
from [7] while enhancing the procedure by evaluating the
quantization effects of the Hardware interfaces (ADC/DAC)
to obtain an accurate discrete-time FWL representation of
the continuous dynamics.

6.

CONCLUSIONS

We have presented a method for synthesizing stable controllers and an implementation in a tool called DSSynth. The
novelty in our approach is that it is fully automated and algorithmically and numerically sound. In particular, DSSynth
marks the first use of the CEGIS that handles plants with
uncertain models and FWL effects over the digital controller.
Implementing this architecture requires transforming the
traditional CEGIS refinement loop into a two-stage engine:
here, the first stage performs fast, but potentially unsound
fixed-point operations, whereas the second stage restores
soundness by validating the operations performed by the first
stage using interval arithmetic. Our experimental results
show that DSSynth is able to synthesize stable controllers
for most benchmarks within a reasonable amount of time
fully automatically. Future work will be the extension of this

CEGIS-based approach to further classes of systems, including those with state space. We will also consider performance
requirements while synthesizing the digital controller.

7.

[19]

REFERENCES

[1] R. Alur, D. Fisman, R. Singh, and A. Solar-Lezama.
SyGuS-Comp 2016: Results and analysis. In Workshop
on Synthesis, volume 229 of EPTCS, 2016.
[2] R. Alur, S. Moarref, and U. Topcu. Compositional
synthesis with parametric reactive controllers. In
HSCC. ACM, 2016.
[3] A. Anta, R. Majumdar, I. Saha, and P. Tabuada.
Automatic verification of control system
implementations. In Embedded Software (EMSOFT),
pages 9–18, 2010.
[4] K. Åström and B. Wittenmark. Computer-controlled
systems: theory and design. 1997.
[5] K. J. Astrom and R. M. Murray. Feedback Systems: An
Introduction for Scientists and Engineers. 2008.
[6] A. Bemporad, M. Morari, V. Dua, and E. N.
Pistikopoulos. The explicit linear quadratic regulator
for constrained systems. Automatica, 38(1), 2002.
[7] I. Bessa, H. Ismail, L. Cordeiro, and J. Filho.
Verification of fixed-point digital controllers using
direct and delta forms realizations. Design Autom. for
Emb. Sys., 20(2), 2016.
[8] I. Bessa, H. Ismail, R. Palhares, L. Cordeiro, and
J. E. C. Filho. Formal non-fragile stability verification
of digital control systems with uncertainty. IEEE
Transactions on Computers, 66(3):545–552, 2017.
[9] E. M. Clarke, D. Kroening, and F. Lerda. A tool for
checking ANSI-C programs. In TACAS, volume 2988,
2004.
[10] S. Das, I. Pan, K. Halder, S. Das, and A. Gupta. LQR
based improved discrete PID controller design via
optimum selection of weighting matrices using
fractional order integral performance index. Applied
Mathematical Modelling, 37(6), 2013.
[11] C. David, D. Kroening, and M. Lewis. Using program
synthesis for program analysis. In LPAR, LNCS, 2015.
[12] J. C. Doyle, B. A. Francis, and A. R. Tannenbaum.
Feedback Control Theory. 1991.
[13] P. S. Duggirala and M. Viswanathan. Analyzing real
time linear control systems using software verification.
In IEEE Real-Time Systems Symposium, Dec 2015.
[14] C. Economakos, G. Economakos, M. Skarpetis, and
M. Tzamtzi. Automated synthesis of an FPGA-based
controller for vehicle lateral control. In MATEC Web of
Conferences, volume 41, 2016.
[15] S. Fadali and A. Visioli. Digital Control Engineering:
Analysis and Design, volume 303 of Electronics &
Electrical. 2009.
[16] I. J. Fialho and T. T. Georgiou. On stability and
performance of sampled-data systems subject to
wordlength constraint. IEEE Trans. on Automatic
Control, 39(12), 1994.
[17] G. Franklin, D. Powell, and A. Emami-Naeini. Feedback
Control of Dynamic Systems. 7th edition, 2015.
[18] S. Ghosh, R. K. Barai, S. Bhattarcharya,
P. Bhattacharyya, S. Rudra, A. Dutta, and R. Pyne.
An FPGA based implementation of a flexible digital
PID controller for a motion control system. In

[20]

[21]

[22]

[23]

[24]

[25]

[26]
[27]

[28]
[29]

[30]

[31]

[32]
[33]

[34]
[35]

[36]

[37]

[38]

Computer Communication and Informatics (ICCCI).
IEEE, 2013.
H. Ismail, I. Bessa, L. C. Cordeiro, E. B. de Lima Filho,
and J. E. C. Filho. DSVerifier: A bounded model
checking tool for digital systems. In SPIN, volume 9232,
2015.
R. Istepanian and J. F. Whidborne. Digital controller
implementation and fragility: A modern perspective.
2012.
S. Itzhaky, S. Gulwani, N. Immerman, and M. Sagiv.
A simple inductive synthesis methodology and its
applications. In ACM Sigplan Notices, volume 45.
ACM, 2010.
S. Jha and S. A. Seshia. SWATI: Synthesizing
wordlengths automatically using testing and induction.
arXiv preprint arXiv:1302.1920, 2013.
L. Keel and S. Bhattacharyya. Robust, fragile, or
optimal? IEEE Trans. on Automatic Control, 42(8),
1997.
L. Keel and S. Bhattacharyya. Stability margins and
digital implementation of controllers. In Proc.
American Control Conference, volume 5, 1998.
G. Klein and B. Moore. Eigenvalue-generalized
eigenvector assignment with state feedback. IEEE
Trans. on Automatic Control, 22(1), 1977.
U. Konigorski. Pole placement by parametric output
feedback. Systems & Control Letters, 61(2), 2012.
Y. Li, K. Ang, G. Chong, W. Feng, K. Tan, and
H. Kashiwagi. CAutoCSD–evolutionary search and
optimisation enabled computer automated control
system design. Int J Automat Comput, 1(1), 2004.
R. E. Moore. Interval analysis, volume 4. 1966.
A. K. Oudjida, N. Chaillet, A. Liacha, M. L.
Berrandjia, and M. Hamerlain. Design of high-speed
and low-power finite-word-length PID controllers.
Control Theory and Technology, 12(1), 2014.
J. Park, M. Pajic, I. Lee, and O. Sokolsky. Scalable
verification of linear controller software. In TACAS.
Springer, 2016.
H. Ravanbakhsh and S. Sankaranarayanan.
Counter-example guided synthesis of control Lyapunov
functions for switched systems. In Conference on
Decision and Control, CDC, 2015.
P. Roux, R. Jobredeaux, and P. Garoche. Closed loop
analysis of control command software. In HSCC, 2015.
R. Schmid, L. Ntogramatzidis, T. Nguyen, and
A. Pandey. A unified method for optimal arbitrary pole
placement. Automatica, 50(8), 2014.
A. Solar-Lezama. Program sketching. STTT, 15(5-6),
2013.
K. Tan and Y. Li. Performance-based control system
design automation via evolutionary computing.
Engineering Applications of Artificial Intelligence,
14(4), 2001.
T. E. Wang, P. Garoche, P. Roux, R. Jobredeaux, and
E. Feron. Formal analysis of robustness at model and
code level. In HSCC, 2016.
W. Wonham. On pole assignment in multi-input
controllable linear systems. IEEE Trans. on Automatic
Control, 12(6), 1967.
J. Wu, G. Li, S. Chen, and J. Chu. Robust finite word
length controller design. Automatica, 45(12), 2009.

