Tuesday, March 18, 2014

ACM has named Leslie Lamport, a Principal Researcher at Microsoft Research Silicon Valley, the recipient of the 2013 ACM A.M. Turing Award for imposing clear, well-defined coherence on the seemingly chaotic behavior of distributed computing systems, in which several autonomous computers communicate with each other by passing messages. He devised important algorithms and developed formal modeling and verification protocols that improve the quality of real distributed systems. These contributions have resulted in improved correctness, performance, and reliability of computer systems.

Lamport's practical and widely used algorithms and tools have applications in security, cloud computing, embedded systems and database systems as well as mission-critical computer systems that rely on secure information sharing and interoperability to prevent failure. His notions of safety, where nothing bad happens, and liveness, where something good happens, contribute to the reliability and robustness of software and hardware engineering design. His solutions for Byzantine Fault Tolerance contribute to failure prevention in a system component that behaves erroneously when interacting with other components. His creation of temporal logic language (TLA+) helps to write precise, sound specifications. He also developed LaTeX, a document preparation system that is the de facto standard for technical publishing in computer science and other fields.

The ACM A.M. Turing Award, widely considered the "Nobel Prize in Computing," carries a $250,000 prize, with financial support provided by Intel Corporation and Google Inc. It is named for Alan M. Turing, the British mathematician who articulated the mathematical foundation and limits of computing, and who was a key contributor to the Allied cryptanalysis of the German Enigma cipher and the German "Tunny" encoding machine in World War II.

ACM will present the 2013 A.M. Turing Award at its annual Awards Banquet on June 21 in San Francisco, California.