We first present a specification language for modelling memory explicitly as an array, and models pointers and data elements uniformly as integers, used here as an abstraction of a machine word. There are three distinguishing features: the use of recursive definitions, the use of set variables representing {\em explicit footprints} in order to implement the concept of {\em separation}, and finally, the language can express the {\em strongest postcondition} of a loop-free program. This provides a basis for implementing a Floyd-Hoare-style program verifier which generates verification conditions for an external theorem prover.
We then present a prover in the form of inference rules that are systematically applied. We argue that a large class of verification conditions can thus be automatically proven. The main novelty is the ability to employ induction hypotheses that are {\it automatically generated} in order to reason about the interplay between recursive definitions, arrays, sets and integers. Finally, recursive definitions are reduced into purely integer formulas, which we can finally dispense with using a standard system.