The techniques of classical abstract interpretation are extended to the big- and small-step operational semantics of higher-order and communicative languages: Well-known techniques, such as memoization, and lesser-known ones, such as abstraction on program syntax, are employed to generate finite abstract interpretations of source programs based on their formal operational semantic definitions. The result is a clear methodology for generating semantically safe (and live) abstract, regular trees for programs that do not possess obvious, finite, state-transition diagram depictions. The primary application of the research is to the validation of program properties; in particular, the application of model checking to validate safety properties in the box-mu calculus and liveness properties in the diamond-mu calculus is discussed.