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

[Michael Anthony Smith]

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.
>
>
>
>
>