An asymmetric satellite equipped with control momentum gyroscopes (CMGs) with the center of mass of the system moving uniformly in a circular orbit was considered. The stability of a relative equilibrium attitude of the satellite was analyzed using Lyapunov’s direct method. The Lyapunov function <em class="EmphasisTypeItalic ">V</em> is a positive definite integral of the total energy of the perturbed motion of the system. The asymptotic stability analysis of the stationary motion of the conservative system was based on the Barbashin-Krasovskii theorem on the nonexistence of integer trajectories of the set <span class="InlineEquation" id="IEq1">\(\dot V\)</span>, which was obtained using the differential equations of motion of the satellite with CMGs. By analyzing the sign definiteness of the quadratic part of <em class="EmphasisTypeItalic ">V</em>, it was found earlier by V.V. Sazonov that the stability region is described by four strict inequalities. The asymptotic stability at the stability boundary was analyzed by sequentially turning these inequalities into equalities with terms of orders higher than the second taken into account in <em class="EmphasisTypeItalic ">V</em>. The sign definiteness analysis of the inhomogeneous function <em class="EmphasisTypeItalic ">V</em> at the stability boundary involved a huge amount of computations related to the multiplication, expansion, substitution, and factorization of symbolic expressions. The computations were performed by applying a computer algebra system on a personal computer.