Sign In

Communications of the ACM

ACM News

ACM Turing Award Goes to Pioneer Who Advanced Reliability and Consistency of Computing Systems


Leslie Lamport, principal researcher at Microsoft Research Silicon Valley.

ACM has named Leslie Lamport, a Principal Researcher at Microsoft Research Silicon Valley, as the recipient of the 2013 ACM A.M. Turing Award.

Credit: Leslie Lamport

ACM (Association for Computing Machinery) today named Leslie Lamport, a Principal Researcher at Microsoft Research Silicon Valley, as 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. 

The ACM Turing Award, widely considered the "Nobel Prize in Computing," carries a $250,000 prize, with financial support provided by Intel Corporation and Google Inc. 

ACM President Vint Cerf noted that "as an applied mathematician, Leslie Lamport had an extraordinary sense of how to apply mathematical tools to important practical problems.  By finding useful ways to write specifications and prove correctness of realistic algorithms, assuring strong foundation for complex computing operations, he helped to move verification from an academic discipline to practical tool."

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.

 

From ACM
View Full Article

 


 

No entries found

Comment on this article

Signed comments submitted to this site are moderated and will appear if they are relevant to the topic and not abusive. Your comment will appear with your username if published. View our policy on comments

(Please sign in or create an ACM Web Account to access this feature.)

Create an Account

Log in to Submit a Signed Comment

Sign In »

Sign In

Signed comments submitted to this site are moderated and will appear if they are relevant to the topic and not abusive. Your comment will appear with your username if published. View our policy on comments
Forgot Password?

Create a Web Account

An email verification has been sent to youremail@email.com
ACM veriŞes that you are the owner of the email address you've provided by sending you a veriŞcation message. The email message will contain a link that you must click to validate this account.
NEXT STEP: CHECK YOUR EMAIL
You must click the link within the message in order to complete the process of creating your account. You may click on the link embedded in the message, or copy the link and paste it into your browser.
Sign In for Full Access
» Forgot Password? » Create an ACM Web Account