This years winners are Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis.
This years winners are recognized for their work on Model Checking:
Model Checking is a type of “formal verification” that analyzes the logic underlying a design, much as a mathematician uses a proof to determine that a theorem is correct. Far from hit or miss, Model Checking considers every possible state of a hardware or software design and determines if it is consistent with the designer’s specifications. Clarke and Emerson originated the idea of Model Checking at Harvard in 1981. They developed a theoretical technique for determining whether an abstract model of a hardware or software design satisfies a formal specification, given as a formula in Temporal Logic, a notation for describing possible sequences of events. Moreover, when the system fails the specification, it could identify a counterexample to show the source of the problem. Numerous model checking systems have been implemented, such as Spin at Bell Labs.
Founder and President of 
Hello, I'm Brian Roy. I'm a father of two beautiful girls, husband to an amazing wife, innovator, entrepreneur and technology geek. 
