[racket] Reading recommendation for static analysis?

Hello everyone,

I am trying to accomplish the following task, and was wondering if anyone
knows of a fitting paper that I can read. I want to write a static analysis
tool for a small scheme-like language to catch simple typing errors. The
following is a simple example of the type of errors that I would like to
detect:

1) let b = (or (pair? x) (string? x))  ;; compute whether x is a pair or a
string
2) assert b   ;; early exit the program if b is false.
3) result = x * 2 ;; <--- This is a type error that can be found using
static analysis.

In words, the pseudocode fragment says:
1) Let b be a boolean, it indicates whether x is a pair or string.
2) Assert that b must be true.
3) Store x times 2 into result. This must be a type error because, for
program execution to reach this point, x must either be a pair or a string,
otherwise the assertion would have failed. Therefore, since x is either a
pair or a string, it is definitely not an integer.

I know the general case is not solvable, but I wish for the tool to detect
as many errors as possible. I am currently looking through the abstract
interpretation and symbolic execution literature. If anyone knows of a
paper that is suitable for my problemd I would be very appreciative.

Thank you very much
  -Patrick
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20120102/1436f73d/attachment.html>