First highlight: One evening Rustan entertained us with lots of puzzles. We managed to solve most (all?) of the ones we discussed. Here's the one I thought was the hardest.
Next I'll tell you how to generate invariants with universal quantifiers by using an interpolating prover, straight from the "best paper" at TACAS.
And now some off topic stuff.
Since we are talking about puzzles, here's another one I saw recently. It was previously featured on xkcd and it is also featured by one of the toilets in the CASL. It didn't excite me before I saw the (intentionally) wrong solution of Terence Tao. The fact that the error is so subtle made me think that I got the correct answer in the first place by accident :)
Unrelated: Any ideas what I should do with my new Google backed (home) page?
No comments:
Post a Comment
Note: (1) You need to have third-party cookies enabled in order to comment on Blogger. (2) Better to copy your comment before hitting publish/preview. Blogger sometimes eats comments on the first try, but the second works. Crazy Blogger.