Amir Pnueli

For seminal work introducing temporal logic into computing science and for outstanding contributions to program and system verification.