enter search term and/or author name
The apprentice challenge
J. Strother Moore, George Porter
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
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...