[PRL] POPL 2004 Virtual Report

[Mitchell Wand]

Well, none of us got to go to POPL, but I finally got around to
scanning the proceedings to identify some papers that might be
interesting to me or others in the lab.  I did that from ICFP '03, and
it felt like a useful exercise to me (though I don't know if it was
useful to others).  So here we go again:

Nick Benton. Simple Relational Correctness Proofs for Static Analyses
and Program Transformations.

"Although static program analyses are routinely proved correct, the
soundness of the optimizing transformations which they enable is much
less frequently addressed.  [Most of the work comes from the
functional community ["especially from the group at Northeastern" :-]]
One might think that this is because the correctnes of most imperative
optimizations is entirely trivil, but what literture there is on the
subject.. indicates that this is not so....  Many transformatioins
involve locally replacing sme part P of a larger program C[P] with a
new version P' which is NOT observationally equivalent to P, but which
IS equivalent in context C..."

Sumii and Pierce. A Bisimulation for Dynamic Sealing

They study what happens if you add to the CBV lambda-calculus a set of
primitives for protecting abstract data by sealing.

Birkedal, Torp-Smith, and Reynolds.  Local Reasoning about a Copying
Garbage Collector.

They prove the correctness of Cheney's copying gc (from 1970) using
Reynolds' separation logic.  This addresses some of the issues that
Dale discussed when he presented this logic earlier this year (eg, gc
was not sound in the logic).

Henzinger, Jhala, Majumdar, McMillan.  Abstractions from Proofs

"The success of model checking for large programs depends crucially on
the ability to efficiently construct parsimonious abstractions. ... We
[show how to] efficiently construct, from a given abstract error trace
which cannot be concretized, a parsimonious abstraction that removes
the trace."  Also check out this sentence, from sectin 6.2: "The main
difficulty when dealing with functions and pointers is in handling the
semantics of calls and returns, because the callee may be passed
pointers into the local space of the caller.  The complexity arises
when we wish to abstract functions polymorphically, because then we
have to summarize all effects that callee may have had on the caller's
store at the point of return"  (Sound familiar?)

Sounds like required reading for anybody interested in pointer
analysis, model checking, or false positives.

Qadeer, Rajamani, and Rehof.  Summarizing Procedures in Concurrent
Programs.  

"The ability to summarize procedures in fundamental to building
scalable interprocedural analyses.  For sequential programs, procedure
summarization is well-understood and used routinely... [hmm,
interesting that they regard this as a solved problem. --Mitch]. In
this paper, we present an intuitive and novel notion of procedure
summaries for multithreaded programs.  Our algorithm can also be
viewed as a precise interprocedural dataflow analysis for
multithreaded programs.

Flanagan and Freund.  "Atomizer: A Dynamic Atomicity Checker for
Multithreaded Programs"

O'Hearn, Yang, and Reynolds.  "Separation and Information Hiding"

They use separation logic to keep track of which portion of the store
each program component can access.  This sounds like it would be of
interest if you were thinking about non-interfering aspects & stuff.

Dreyer.  A Type System for Well-Founded Recursion.

How to prove that your recursive module system doesn't fail to
terminate at module-construction time.  Based on the "Scheme
'backpatching' semantics.