Dave (![[info]](http://p-stat.livejournal.com/img/userinfo.gif){kind=small} dga) wrote,@ 2008-02-04 13:10:00 |
|
CMU Turing awards += 1
In very cool news today, I just spotted on my department head's blog (okay, can I admit here that it's cool to have a department head who keeps a blog? I actually know what's going on these days) that a fellow faculty member at CMU, Ed Clarke, was selected for the ACM Turing Award.
(For the one non-computer-geek who reads this: The Turing award is roughly the equivalent of the nobel for computer scientists--there's no Nobel for CS. It comes with a pile of recognition and a comfortable pile of cash, about $250,000 this year. Prior Turing award winners include some of the only household names from computer science -- Rivest, Shamir, and Adleman, more familiarly known as the initials in the RSA public key algorithm, and Cerf & Kahn, the variously-named parental units of the Internet.)
What I think is particularly cool about the award is the reason it's being given: Ed's receiving the award for his work in formal verification. Basically, he designs ways to automatically check whether hardware and software designs will work properly. The problem is both cool and hard: It's easy to run lots of tests against something and say "well, it doesn't seem to have crashed so far", but how do you know that you've tested everything? Intel has a pretty amazing apparatus for testing their designs, but that didn't prevent the 1994 floating point division bug in the Pentium. Formal verification instead develops mechanisms to prove that a design has some particular property---such as that it always gets the right result when it adds two numbers together.
Formal verification has taken root in hardware designs, but only more recently has it started making (small) inroads into software. It's a tough problem, but as software becomes even more critical (is that possible?) to our lives, I think we'll see a slowly increasing uptake of verification for software. For those of you whose browsers crashed while reading this post, the bad news is that it won't be overnight.
In very cool news today, I just spotted on my department head's blog (okay, can I admit here that it's cool to have a department head who keeps a blog? I actually know what's going on these days) that a fellow faculty member at CMU, Ed Clarke, was selected for the ACM Turing Award.
(For the one non-computer-geek who reads this: The Turing award is roughly the equivalent of the nobel for computer scientists--there's no Nobel for CS. It comes with a pile of recognition and a comfortable pile of cash, about $250,000 this year. Prior Turing award winners include some of the only household names from computer science -- Rivest, Shamir, and Adleman, more familiarly known as the initials in the RSA public key algorithm, and Cerf & Kahn, the variously-named parental units of the Internet.)
What I think is particularly cool about the award is the reason it's being given: Ed's receiving the award for his work in formal verification. Basically, he designs ways to automatically check whether hardware and software designs will work properly. The problem is both cool and hard: It's easy to run lots of tests against something and say "well, it doesn't seem to have crashed so far", but how do you know that you've tested everything? Intel has a pretty amazing apparatus for testing their designs, but that didn't prevent the 1994 floating point division bug in the Pentium. Formal verification instead develops mechanisms to prove that a design has some particular property---such as that it always gets the right result when it adds two numbers together.
Formal verification has taken root in hardware designs, but only more recently has it started making (small) inroads into software. It's a tough problem, but as software becomes even more critical (is that possible?) to our lives, I think we'll see a slowly increasing uptake of verification for software. For those of you whose browsers crashed while reading this post, the bad news is that it won't be overnight.
