The highlight of the day for me (and with the greatest respect to the other speakers) was Ken McMillan's invited lecture. Wow - this was one of the best invited talks I've been to! Ken explained the notion of "relevance heuristics" in program analysis.
He started by considering abstractly one of the key tensions faced by program analyses: the tension between precision on the one hand and scalability on the other. For example, imagine we have two facts at some merge point. In analyses based on least fixed points we typically lose information at merge points (a loss of precision); in analyses based on predicate abstraction we form a disjunction (which is precise but does not scale). Can we do better?
His insight is to be inspired by techniques used by modern SAT solvers. They exhibit a form of laziness in that they only resolve clauses when model search fails and they also learn from the past. [And lots more!]
Ken then showed how these techniques can be adapted to program analysis: one of the key tools is a use of Craig's interpolation lemma in the refinement process.
What was most impressive about the talk was that it really captured the entire audience's attention. Peanut-brained researchers like me followed the start and could see what was happening in the later parts, but also the real experts in the room (Tom Ball, Byron, ...) all seemed to be concentrating hard as the material got tough too. To keep everyone happy is a real achievement.
Thanks, Ken.
The day finished with a very nice meal at Cafe Kati - a Cal-Asian restaurant (hadn't heard of that before) - with Peter, Matt, Mike and Alex.
skip to main |
skip to sidebar
No comments:
Post a Comment