As others have pointed out there is a lot of existing research into formal methods for program analysis. A former colleague of mine is an active researcher in this area and his page gives several pointers on where to start.
There are several keywords in that area, each of which basically spawns a whole research area itself. Hence, your question cannot be fully answered here, but we can at least provide some direction. For the most part, these approaches are separated into three branches:
- Algebraic semantics are one way of giving semantics to programming languages via different algebras. See the wikipedia article for an overview. Things like Kleene algebras or Omega algebras fit in there.
- Operational semantics are quite popular calculi to model behaviors (for example, the lambda calculus, or LISP)
- Denotational semantics rely on a fitting domain. They include, for example, approaches rooted in predicate or linear logic (think Prolog or more advanced languages like CHR).
And just like in physics we are also interested in unifying these branches, at which point you enter the realms of the unified theories of programming.
Sorry for not giving a specific answer to the question, but there's enough material available for all of this to keep you busy for a few decades, and unless a desired application is in mind it's not really possible to make a choice from these.