It appears to me that the gist of your suggestion is to translate a program into a relation and reason about the transitive closure of that relation. It is orthogonal that this relation is definable in first order arithmetic. 

The idea of translating a program into a relation is rather old and I doubt there is a unique reference for it. I will share what I know, but in each case, there are surely older papers. The first paper below suggests modelling programs as transition systems and reasoning about them. Plotkin's paper provides a way to inductively derive a transition system from program text (though the idea is much older, I'm sure).

 1. Robert Keller, 1976, *Formal verification of parallel programs*. 
 2. Gordon Plotkin, 1981. *Structural Operational Semantics.* 

The transition system is essentially the relation you describe. The transitive closure is a fixed point over this relation. It is one of several objects that can be defined by fixed points. Reasoning about properties of programs using fixed points is very old too.

 4. David M. R. Park, 1969, *Fixpoint induction and proofs of program properties*. 
 5. Lawrence Flon and Norihisa Suzuki, 1975, *Consistent and Complete Proof Rules for the Total Correctness of Parallel Programs*.
 6. Patrick Cousot and Radhia Cousot, 1977, *Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints*.

Finally, there is a precise mathematical sense in which the fixed point (or transitive closure) approach is not significantly different from Floyd/Hoare logic. 

 7. Edmund M. Clarke Jr., 1977, *Program Invariants as Fixed Points*.

To quote from the abstract of the paper:

> We argue that soundness and relative completeness theorems for Floyd-Hoare Axiom Systems ([3], [5], [18]) are really fixedpoint theorems. We give a characterization of program invariants as fixedpoints of functionals which may be obtained in a natural manner from the text of a program. We show that within the framework of this fixedpoint theory, soundness and relative completeness results have a particularly simple interpretation. Completeness of a Floyd-Hoare Axiom System is equivalent to the existence of a fixedpoint for an appropriate functional, and soundness follows from the maximality of this fixedpoint. 


Reasoning about programs by computing fixed points is extremely standard in practice. Rather than relations, we tend to deal with a transformer defined by a relation, such as a predicate or state transformer.  If you are genuinely committed to reasoning over relations in a logic, you will require transitive closure logics because properties like graph reachability are not first order definable. I can point to this recent paper, but you will have to dig around for older ones.

 1. Neil Immerman, Alexander Rabinovich, Thomas W. Reps, Mooly Sagiv, and Greta Yorsh, 2004, *The Boundary Between Decidability and Undecidability for Transitive Closure Logics*.


Edit: Adding a link.

You might want to try the following verifiers that use a combination of automated reasoning and fixed point techniques. Though they may fail on harder examples, they can still discover useful invariants and errors.

 1. [Interproc][1]
 2. [Pex][2]


  [1]: http://pop-art.inrialpes.fr/interproc/interprocweb.cgi
  [2]: http://www.pexforfun.com/Default.aspx?language=CSharp&sample=AbsVerified