A well-known result due to J. T. Stafford asserts that a stably free left module M over the Weyl algebras D = An(k) or Bn(k) − where k is a field of characteristic 0 − with rankD(M) ≥ 2 is free. The purpose of this paper is to present a new constructive proof of this result as well as an effective algorithm for the computation of bases of M. This algorithm, based on the new constructive proofs (Hillebrand and Schmale, 2001; Leykin, 2004) of J. T. Stafford’s result on the number of generators of left ideals of D, performs Gaussian elimination on the formal adjoint of the presentation matrix of M. We show that J. T. Stafford’s result is a particular case of a more general one asserting that a stably free left D-module M with rankD(M) ≥ sr(D) is free, where sr(D) denotes the stable rank of a ring D. This result is constructive if the stability of unimodular vectors with entries in D can be tested. Finally, an algorithm which computes the left projective dimension of a ge...