Early References for Transition System Semantics of Programs I am trying to trace back the origins of transition system semantics for imperative programs. I am assuming a transition system is a tuple $(\mathit{States}, \mathit{Trans})$ consisting of a set of states and a (binary) transition relation over states. By transition system semantics, I mean that there should be a mapping from programs to transition systems. 

The presentation need not be exactly as I describe above and the mapping from programs to transition systems need not be completely explicit. For example, I would consider Plotkin's Structural Operational Semantics as providing transition system semantics to a formal language. Other early references I know of are due to Cousot &amp; Cousot, and even earlier, due to Robert Keller in Formal Verification of Parallel Programs. There is earlier work by Richard Karp and Raymond Miller on reasoning about parallel programs, but their model is closer to Petri Nets and I am unsure about whether to read their paper as giving transition system semantics to programs.

Does anyone know of references from the early 80s or earlier where transition system semantics are provided for programs? Please add a few lines about the semantics and whether it is used today, and in what form.
Landin's SECD machine, originally described in The mechanical evaluation of expressions in 1964, is a transition system in the form of an abstract machine, later inspiring lots of of other abstract machines such as the CESK machine.