Determining whether a program is equivalent to another using its source code is probably a little bit hard to solve the problem. Usually a program has a programming paradigm according to its programming language. Probably the main conflict finding equivalences between two programs is the fact that we cannot use an approach based on its execution and expected results. Recently on a blog post on programando.org a problem related to find the equivalence between two programs was proposed as programming challenge, but the problem is not related to algorithm equivalence, which seems that it is not solved yet. There are several approaches on the equivalence between two programs. Now in this post, I am just rambling about the ideas that are coming to my mind about this problem.
We have beta equivalences, which means that translating the code to Lambda Calculus functions, we can find if two programs can be derived into the same final function using beta reductions. Expressing labels in some functional language is not so hard as you think. Guy Steele already have proposed a grammar to express labels as are they presented on the Fortran code in the examples of the challenge. Even if, that syntax is not present on the functional programming language, you can use maps and graphs to hold both labels and code, because you can bind functions to variables in functional languages. So, expressing labels as maps and graphs is not a problem. So, each code segment in the Fortran code should have an unique representation as function, and you should have same reduction once you process the code.
Another idea comes to my mind. The complete code can be represented as a tree, and we have a common approach called Abstract Syntax Tree, which is a directed graph. Very similar to what I have designed to parse the L-System DSL made for a previous contest on programando.org. Also, two directed graphs are equal if they have the same order in their nodes. This makes a difference. So, it should be a kind of sorted directed graph, but using some kind of identities between graph nodes related to its composition, rather their node keys. We can use some kind of checksum or hash on each node, like the hash function on Python or the hash method on Java, but avoiding label names and variable names, holding only calls, constants and control statements. The final hash or checksum should be equal on both programs.
So, would be nice to implement a program meeting both equivalences, the beta reduction and the AST hash. Including the brute force testing algorithm interpreting the program and comparing the execution results. I think that will be implementing the problem in three stages, first I will check the AST, because I am forced to build it first to parse the program. Then I will try to implement the beta reduction and finally I will try to implement the interpreter. I really like how parser combinators can help on this kind of problems; you can quickly define a DSL when you need it.
Entries 
Are there any restrictions that make this treatable? If there are no restrictions, you could write the following two programs (using pseudo-code):
(1) print “done”
(2) n = 3 (or greater)
for a,b,c taking all possible integers
if a^n + b^n = c^n then print “done” and exit
(1) and (2) would only be equivalent if Fermat’s last theorem was wrong, and your program would be able to prove this.
In a more practical scenario, you could assume that since the number of integers you can try is limited (by the type, or by the memory), (2) will finish at some point and allow you to conclude, not actually proving that there is no solution for the n you chose.
If you can assume that both programs finish, it becomes easier, since you can emulate both and see the result.
Another restriction that makes it tractable is to assume a memory limit for the programs. This will give a finite number of configurations, and allow you to determine it a program will finish or not. Anyways, that is quite expensive, since you have to keep track of all the possible states that arise within the acceptable parameters.
Good luck with the challenge, it will be very interesting to know how the proposed solutions work under tricky cases, and which heuristics they implement :-).