The second part of the summer school was a bit more applied and more in the direction of my own interests. Chandra Krintz talked about managed runtime environments. Yannis Smaragdakis introduced multi-threaded programming and transactional memory. Sumit Gulwani as the third lecturer taught us symbolic bounds computation.
As a cherry on the cake, Oliver Danvy talked about general tips and tricks for PhD students.
Managed Runtime Environments: Implementations and Opportunities
The content-part of her lecture started with an overview of how VMs execute programs. Well, as usual, it was limited to Java, Python, and Ruby. This gives me the feeling, that there are only very few people looking into the similarities between runtimes for functional and imperative languages. She talked about stack-based VM instruction sets and briefly mentioned register-based as well as register-memory-based designs, but mainly referring to CPU instruction set architectures. Interpretation techniques, just-in-time compilation, problems associated with profiling and instrumentation had been discussed, but neither of them in detail.
One topic, she was spending more time on was her own research, i.e., communication between independent JVM instances via shared memory. It was interesting, especially her approach to share classes between the VM instances by using shared pages and direct pointers from the instances.
The last lecture was a broad overview of cloud computing, available techniques and the current challenges, but not really technical.
Multi-Threaded Programming and Transactional Memory
Yannies gave more or less a hands-on introduction to locks and threads with programming examples/exercises. From the poll in the audience, there are actually people, which never have used threads before. I thought this is just one of the assumptions professors usually get wrong, but well… From my point of view, I have heard a lot of it already before, but it was still nice to be reminded of some of the details we discussed. The primitives for monitor-style/traditional shared-memory concurrency he identified were lock/unlock, wait, signal, and broadcast. They allow building any kind of more complex critical sections on top.
The basic points he emphasized are to use while-loops on all conditions and the rule for single signals vs. broadcast signals. In short, a single signal, i.e., a notify, can only be used when all threads waiting on a condition are equal, but only one at a time can make progress. If more then one can make progress, a broadcast, i.e., a notifyAll has to be used to avoid livelocks.
After some typical examples of problems with locks, for instance, locking order leading to deadlocks, he introduced transactional memory. His focus was on the implications of this programming model, the different variations, performance questions, and the problem of irreversible operations.
Art of Invariant Generation applied to Symbolic Bound Computation
The computation of bounds for e.g. loops has a broad range of applications. The knowledge about bounds allows estimating the necessary runtime or memory utilization, thus in general resource utilization. Furthermore, it can be used to identify secrecy properties in terms of information leakage due to repetitive patterns and problems of robustness due to errors and uncertainty for instance introduced by rounding.
After a short introduction and a simple example, he introduced a countless number of approaches to this problem and explained how to apply them to specific problems. His lectures was stuffed with a lot of content, think much more then any other lecturer tried to convey. Moreover, he managed to speak with an incredible speak. Have never heard someone before, putting an infinite number of words into one minute. Sometimes less is more…
Edutainment for the Night Lecture
Oliver was giving a Tips and Tricks lecture about being a PhD student, writing and reviewing papers, and giving talks. Presented in a quite entertaining style 
I started as a PhD student in October 2008 at the