ACM DL

Programming Languages and Systems (TOPLAS)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 24 Issue 3, May 2002

The apprentice challenge
J. Strother Moore, George Porter
Pages: 193-216
DOI: 10.1145/514188.514189
We describe a mechanically checked proof of a property of a small system of Java programs involving an unbounded number of threads and synchronization, via monitors. We adopt the output of the javac compiler as the semantics and verify the system at...

Parametric shape analysis via 3-valued logic
Mooly Sagiv, Thomas Reps, Reinhard Wilhelm
Pages: 217-298
DOI: 10.1145/514188.514190
Shape analysis concerns the problem of determining "shape invariants" for programs that perform destructive updating on dynamically allocated storage. This article presents a parametric framework for shape analysis that can be instantiated in...