[gclist] Finalization, again

[Tim Hollebeek]

> From: Fergus Henderson [mailto:fjh@cs.mu.oz.au]
>
> On 06-Oct-2001, David Chase <chase@world.std.com> wrote:
> > At 12:09 PM 10/5/2001 +0100, Nick Barnes wrote:
> > >Proof-carrying code, Necula et al, addresses exactly this sort of
> > >point.  You need to know that some code (e.g. a downloaded 
> applet) has
> > >certain properties (runs in a given amount of time, doesn't perform
> > >"illegal" accesses, doesn't raise exceptions).  So you require that
> > >the code should come with a proof of these properties.  
> You can check
> > >the proof in a small finite time.  Generating such a proof is very
> > >much harder(!).
> > 
> > How hard is it?  (I suppose there's papers I should read.)

See http://www.cs.berkeley.edu/~necula/pcc.html.

>From what I recall, memory/type safety is pretty easy to handle; anything
more complex is substantially harder.

Tim Hollebeek
Research Scientist
Cigital Labs