Orna Grumberg (Hebrew : ארנה גרימברג; born May 14, 1952) is an Israeli computer scientist and academic, the Leumi Chair of Science at the Technion.
Hebrew is a Northwest Semitic language native to Israel; the modern version of which is spoken by over 9 million people worldwide. Historically, it is regarded as the language of the Israelites and their ancestors, although the language was not referred to by the name Hebrew in the Tanakh. The earliest examples of written Paleo-Hebrew date from the 10th century BCE. Hebrew belongs to the West Semitic branch of the Afroasiatic language family. Hebrew is the only living Canaanite language left, and the only truly successful example of a revived dead language.
Grumberg is noted for developing model checking, a method for formally verifying hardware and software designs.With Edmund M. Clarke and Doron A. Peled, she is the author of the book Model Checking (MIT Press, 1999).
In computer science, model checking or property checking is, for a given model of a system, exhaustively and automatically checking whether this model meets a given specification. Typically, one has hardware or software systems in mind, whereas the specification contains safety requirements such as the absence of deadlocks and similar critical states that can cause the system to crash. Model checking is a technique for automatically verifying correctness properties of finite-state systems.
Edmund Melson Clarke, Jr. is an American retired computer scientist and academic noted for developing model checking, a method for formally verifying hardware and software designs. He is the FORE Systems Professor of Computer Science at Carnegie Mellon University. Clarke, along with E. Allen Emerson and Joseph Sifakis, is a recipient of the 2007 Association for Computing Machinery A.M. Turing Award.
In 2013 Prof. Grumberg was elected to the Academia Europaea.In 2015 she was named a Fellow of the Association for Computing Machinery "for contributions to research in automated formal verification of hardware and software systems."
The Academia Europaea is an independent learned society and European Union’s Academy of Humanities and Sciences.
In computer science, specifically software engineering and hardware engineering, formal methods are a particular kind of mathematically based technique for the specification, development and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.
Leslie B. Lamport is an American computer scientist. Lamport is best known for his seminal work in distributed systems and as the initial developer of the document preparation system LaTeX. Leslie Lamport was the winner of the 2013 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.
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.
Amir Pnueli was an Israeli computer scientist and the 1996 Turing Award recipient.
David Harel is a computer scientist at the Weizmann Institute of Science in Israel, and holds the William Sussman Professorial Chair of Mathematics. Born in London, England, he was Dean of the Faculty of Mathematics and Computer Science at the institute for seven years. He currently also serves as Vice-President of the Israel Academy of Sciences and Humanities.
Moshe Ya'akov Vardi is an Israeli mathematician and computer scientist. He is a Professor of Computer Science at Rice University, United States. He is the Karen Ostrum George Professor in Computational Engineering, Distinguished Service Professor, and Director of the Ken Kennedy Institute for Information Technology. His interests focus on applications of logic to computer science, including database theory, finite-model theory, knowledge in multi-agent systems, computer-aided verification and reasoning, and teaching logic across the curriculum. He is an expert in model checking, constraint satisfaction and database theory, common knowledge (logic), and theoretical computer science.
Yuri Gurevich is an American computer scientist and mathematician and the inventor of abstract state machines. He is Principal Researcher at Microsoft Research, where he founded the Foundations of Software Engineering group, and he is professor emeritus at the University of Michigan.
Nir Shavit is an Israeli computer scientist. He is a Professor in the Computer Science Department at Tel Aviv University and a Professor of Electrical Engineering and Computer Science at the Massachusetts Institute of Technology.
Marta Zofia Kwiatkowska is a Polish computer scientist based in the United Kingdom. She is professor of computing systems in the Department of Computer Science at the University of Oxford, England, and a Fellow of Trinity College, Oxford.
Monika Henzinger is a German computer scientist, and is a former director of research at Google. She is currently a professor at the University of Vienna. Her expertise is mainly on algorithms with a focus on data structures, algorithmic game theory, information retrieval, search algorithms and Web data mining. She is married to Thomas Henzinger and has three children.
Assaf Schuster is an Israeli professor of computer science whose works have been published in such journals as Computer Aided Verification and Journal of Systems and Software. Schuster earned his Ph.D. from the Hebrew University of Jerusalem in 1991, under the supervision of Eli Shamir. Currently he works at Technion – Israel Institute of Technology.
Cherri M. Pancake is an ethnographer and computer scientist who works as a professor of electrical engineering and computer science and Intel Faculty Fellow at Oregon State University, and as the director of the Northwest Alliance for Computational Science & Engineering. She is known for her pioneering work on usability engineering for high performance computing. In 2018 she was elected for a two-year term as president of the Association for Computing Machinery.
Yoelle Maarek is a vice president at Amazon, responsible for Amazon's Alexa Shopping Research.
Yuanyuan (YY) Zhou is a Chinese and American computer scientist and entrepreneur. She is a professor of computer science and engineering at the University of California, San Diego, where she holds the Qualcomm Endowed Chair in Mobile Computing. Her research concerns software reliability, including the use of data mining to automatically detect software bugs and flexible system designs that can adapt to hardware platform variations. She is also the founder of three start-up companies, Emphora, Pattern Insight, and Whova.
Rina Dechter is a Professor of Computer Science in the Donald Bren School of Information and Computer Sciences at University of California, Irvine. Her research focuses on automated reasoning and constraint satisfaction in artificial intelligence. In 2013, she was elected a Fellow of the Association for Computing Machinery.
Pamela Zave is an American computer scientist now working at Princeton University. She is known for her work on requirements engineering, telecommunication services, and protocol modeling and verification, and is now working on network architecture. She was named a Fellow of the Association for Computing Machinery in 2002, and was the 2017 recipient of the Harlan D. Mills Award from the IEEE Computer Society.
Alexander Vardy is a Russian-born and Israeli-educated electrical engineer known for his expertise in coding theory. He holds the Jack Keil Wolf Endowed Chair in Electrical Engineering at the University of California, San Diego. The Parvaresh–Vardy codes are named after him.
Joost-Pieter Katoen is a Dutch theoretical computer scientist based in Germany. He is distinguished professor in Computer Science and head of the Software Modeling and Verification Group at RWTH Aachen University. Furthermore, he is part-time associated to the Formal Methods & Tools group at the University of Twente.