An algorithm is outlined for deciding the correctness of bounded space and time imperative programs, using linear algebra techniques encoded in the theory of real closed fields. The approach is shown to be feasible for classical, probabilistic and quantum programs. Joint work with P. Mateus, J. Ramos and C. Sernadas.