symbolic similation/abstract execution of procedural languages

[Ramchandani Rajen Sham]

I am looking for any code that will enable me to perform symbolic simulation/
abstract execution of any high level procedural language. It would be 
nice if it has the capability of resolving brach conditions whenever 
possible.  Or on the other hand if you have some program that is capable of 
deciding if a statement is true or false depending on the conditions it
has seen so far i would like to hear from you. 

what is mean is: given the following hypothetical code fragment

sum = 0; 
loop 
  read ( x, y);                                                  -(1)
  if x > 2 then sum = sum + x - 2 else sum = sum + x ;           -(2)
  if y > x && y > 2 then sum = sum + y - 2 else sum = sum + y;   -(3)
end loop 

the executer would trace a path thus 
PC(1): input x1, y1;
PC(2): ( x1 > 2 AND  sum = x1 - 2 )  OR
       (x1 <= 2 AND sum = x1) 
PC(3): ( x1 > 2 AND  sum = x1 - 2)  AND (y1 > x1 && y1 > 2  
                                           AND sum = sum + y1 -2 )
       pruned to ( x1 > 2 AND  y1 > x1 AND sum = x1 + y1 -4) by the resolver
[ i.e it was able to deduce that y1 >2 was redundant]
OR ( ...............................) 

The last thing on this wish list of mine is if you have some program that
generates input data values  to satisfy a given set of conditions, will be
equalities, inequalities and contain boolean operations. 

If you have any pointers to similar  work being done elsewhere i could like
to hear from you.

Thanks a lot
rajen at edsel.ece.cmu.edu