[TYPES] Query: Types for post-development analysis?

[Michael Hicks]

Many, if not all, of these are examples of so-called "type-based  
analysis" in which reasoning about a program is set up as a type  
system rather than as a problem in model checking, abstract  
interpretation, data flow analysis, etc.  Jens Palsberg has a page on  
this topic that contains pointers to many papers (though it appears  
somewhat dated): http://www.cs.ucla.edu/~palsberg/tba/

There is a survey paper he wrote on this topic that is quite  
accessible: http://www.cs.ucla.edu/~palsberg/tba/papers/palsberg- 
paste01.pdf

-Mike


On Mar 9, 2006, at 5:20 AM, Michael Anthony Smith wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
> types-list ]
>
> Clarification and Summary (so far)
>
> I have already had several useful replies to this original posting
> (thanks). But, from some of these replies it is clear that it is worth
> clarifying my use of the "post-development analysis context", thus  
> I am
> enclosing a description that I sent individually to one of the list  
> members.
>
> By "the post-development analysis context" I mean the analysis of an
> existing product (program), typically by a third party (such as a
> certifier) who has to satisfy themselves that the product meets  
> certain
> criteria (such as showing the absence of bypassing a security  
> manager or
> exception free execution).  It is assumed that such third parties have
> little control over the development process or languages used to
> implement a product.  They may even have little sight of the  
> development
> documentation (or even the source code).  But for the purposes of my
> initial question, lets assume that both the design documentation and
> source code are available.
>
> Having said this, another member of the list provided their own
> interpretation, which is also valid, namely, "someone has already
> written a program in a weakly-typed language but then [wants] to  
> analyze
> that program for further properties using types? ".
>
> Thanks for your responses, I am now in the process of following up the
> pointers you have given me. In summary, the (public*) pointers  
> include:
> @ Work on index type systems (independently invented by Christopher
> Zenger and Hongwei Xi in the 90's).
> @ The *PURe Project (*Program Understanding and Re-engineering:  
> Calculi
> and Applications)  which apply formal methods "in-reverse". Project
> homepage http://wiki.di.uminho.pt/wiki/bin/view/PURe
> @ "Anno Domini", which used types to analyze COBOL programs for
> year-2000 issues. From Type Theory to Year 2000 Conversion Tool
> http://citeseer.ist.psu.edu/eidorff99annodomini.html
> @ Raghavan Komondoor, G. Ramalingam, Satish Chandra, John Field,
> "Dependent Types for Program Understanding", in the Proceedings of  
> TACAS
> 2005, LNCS 3440, Springer Berlin / Heidelberg, 2005. (analyzing COBOL
> programs).
> @ Jeff Foster's (UMD) CQual language, which does "type qualifier"
> inference to find security flaws and other things in C programs. CQual
> homepage http://www.cs.umd.edu/~jfoster/cqual/
> @ Necula's (UC Berkeley) CCured project that does another kind of type
> inference for the purpose of making C programs memory safe. Project  
> home
> page http://manju.cs.berkeley.edu/ccured/
> <http://freshmeat.net/redir/ccured/37987/url_homepage/ccured> (Tool
> available from http://freshmeat.net/projects/ccured/).
>
> *I have only included those pointers that I believe were referencing
> publicly available information. And I have removed the names of the
> correspondents as I have not asked their permission to quote them.
> (Having said this, I will happily give credit if they like; this  
> can be
> done in hindsight, whereas mentioning them publicly cannot easily be
> retracted).
>
> Thanks for your help,
>
> Anthony.
>
> Michael Anthony Smith wrote:
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
>> types-list ]
>>
>> I have been a (silent) member of the types list for several years,  
>> as I
>> am interested in monitoring (and hopefully using) developments in  
>> type
>> theory. I certainly make use of (reasonably) strongly types
>> specification and programming languages in my work, which is  
>> regularly
>> involving the analysis of third party designs/code. Within this  
>> context
>> it is often hard to use developments in the type-theory, as they  
>> appear
>> (at least to me) to be aimed at designing solid development languages
>> and frameworks.
>>
>> I know that type systems are used to design languages (and  
>> frameworks)
>> that have a given collection of desirable properties, whether this be
>> the traditional "shape" correctness or for some other concern such as
>> guaranteeing various concurrency or security properties. I also am  
>> aware
>> of the link between type theories and abstract interpretation. What I
>> was wondering if anyone here knows of the application of type  
>> theories
>> to the post-development analysis context?
>>
>> Thanks,
>>
>> Anthony.
>>
>>
>>
>>
>>