A simple but complete set of algebraic laws is given for a basic language (e.g., at the level of boogie). They include the algebraic properties of concurrency, similar to those of sequential composition. The laws are valid equally for interleaved concurrency and separated concurrency, and mixtures between them (e.g., as used in VCC). Most recognised methods of program analysis and verification are simply derived from the algebra. But will it be useful?