  Let CMSO denote the counting monadic second order logic of graphs. We give a
constructive proof that for some computable function $f$, there is an algorithm
$\mathfrak{A}$ that takes as input a CMSO sentence $\varphi$, a positive
integer $t$, and a connected graph $G$ of maximum degree at most $\Delta$, and
determines, in time $f(|\varphi|,t)\cdot 2^{O(\Delta \cdot t)}\cdot
|G|^{O(t)}$, whether $G$ has a supergraph $G'$ of treewidth at most $t$ such
that $G'\models \varphi$. The algorithmic metatheorem described above sheds new
light on certain unresolved questions within the framework of graph completion
algorithms. In particular, using this metatheorem, we provide an explicit
algorithm that determines, in time $f(d)\cdot 2^{O(\Delta \cdot d)}\cdot
|G|^{O(d)}$, whether a connected graph of maximum degree $\Delta$ has a planar
supergraph of diameter at most $d$. Additionally, we show that for each fixed
$k$, the problem of determining whether $G$ has an $k$-outerplanar supergraph
of diameter at most $d$ is strongly uniformly fixed parameter tractable with
respect to the parameter $d$. This result can be generalized in two directions.
First, the diameter parameter can be replaced by any contraction-closed
effectively CMSO-definable parameter $\mathbf{p}$. Examples of such parameters
are vertex-cover number, dominating number, and many other
contraction-bidimensional parameters. In the second direction, the planarity
requirement can be relaxed to bounded genus, and more generally, to bounded
local treewidth.
