The C-light is a project aimed onto deductive verification of C programs. It relies on three basic ideas, namely—metageneration of verification conditions (MetaVCG), semantic mark-up and the symbolic method, two-level verification that uses C-light language as a front-end and C-kernel language as a back-end. The semantic mark-up extends the standard Hoare inference rules by semantic labels for explanations of failed verification conditions. The symbolic method is based on a replacement of each for-loop by a single assignment with a cumulative effect, it allows us to avoid explicit invariant generation. However, to make verification efficient, it is necessary to develop new techniques instead of the replacement. These new techniques for verification of linear algebra programs is presented and explained in this article.