From the Turing Award announcement, it was for his (and others') work on symbolic model checking: https://web.archive.org/web/20090417205051/http://usacm.acm.o

From the Turing Award announcement, it was for his (and others') work on symbolic model checking: https://web.archive.org/web/20090417205051/http://usacm.acm.org/usacm/weblog/index.php?p=572 https://web.archive.org/web/20090417205051/http://usacm.acm.... I've never used a symbolic model checker (might in the near future!) but as opposed to finite state model checkers which explore every possible system state with breadth-first search, symbolic model checkers can sometimes render the combinatorial explosion of system states tractable. I have heard symbolic model checkers are not a completely free lunch and struggle with deep state graphs even if the branching factor isn't very high.