[racket] Reading recommendation for static analysis?

From: Benderjg2 (benderjg2 at aol.com)
Date: Tue Jan 3 00:08:33 EST 2012

Also, if control flow analysis is relevant to what you are doing, I'd suggest searching for the web sites of Matthew Might and David van Horn. They've done some of the most recent research in that area.

Jim

On Jan 2, 2012, at 10:31 PM, Benderjg2 <benderjg2 at aol.com> wrote:

> Patrick,
> 
> "State of the art" in type-checking Scheme is TypedScheme/TypedRacket. I would suggest checking out the relevant papers at the NEU Racket site:
> http://www.ccs.neu.edu/scheme/pubs/
> 
> For older research on both typing Scheme (e.g. Soft typing) and static analysis of Scheme, I suggest checking the "compilation" page on my Readscheme website:
> http://library.readscheme.org/page8.html
> 
> Others may have mode specific recommendations... I am bibliographer, not a researcher :)
> 
> Cheers,
> Jim
> 
> Sent from my iPad
> 
> On Jan 2, 2012, at 8:40 PM, Patrick Li <patrickli.2001 at gmail.com> wrote:
> 
>> 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
>> ____________________
>> Racket Users list:
>> http://lists.racket-lang.org/users



Posted on the users mailing list.