Edmund M. Clarke

Edmund M. Clarke (1945-2020) was an American computer scientist and pioneer in the field of formal verification. He developed the symbolic model checking technique, which revolutionized the verification of hardware and software systems. Clarke's work has had a profound impact on the advancement of formal methods and the reliability of complex computing systems.

Renowned computer scientist and a pioneer in the field of formal verification. Clarke is widely known for his co-invention of model checking, a technique for verifying hardware and software systems. His seminal work, including the influential paper "Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications," has laid the foundation for the development and advancement of model checking. Clarke's contributions have revolutionized the field of formal methods and played a crucial role in ensuring the correctness and reliability of complex computer systems.

Edmund Melson Clarke, Jr. was an American computer scientist and academic noted for developing model checking, a method for formally verifying hardware and software designs. He was the FORE Systems Professor of Computer Science at Carnegie Mellon University. Clarke, along with E. Allen Emerson and Joseph Sifakis, received the 2007 ACM Turing Award.

• Allen Emerson and Joseph Sifakis, received the 2007 ACM Turing Award.