A Lattice of Languages is a Verification Buffet - 16th June 2015 Imperative Reasoning is Hard - 13th November 2013