{"id":"mooly-sagiv","title":"Mooly Sagiv","content":"**Mooly Sagiv**, also known as **Shmuel Sagiv**, is the the Chief Scientist at Certora, a company he co-founded to scale the application of formal verification in enhancing the security of [smart contracts](https://iq.wiki/wiki/smart-contract) in the blockchain sector. [\\[1\\]](#cite-id-FgmgJZygNQOBq8qP)  [\\[11\\]](#cite-id-r8eOFTRqd7j8Yu2e) \n\n## Early Life and Education\n\nMooly Sagiv was born in Israel and demonstrated an early aptitude for mathematics and computer science. He pursued his higher education at the Technion - Israel Institute of Technology, where he completed his Ph.D. in Computer Science in 1991. His doctoral research laid the groundwork for his future innovations in software verification. [\\[2\\]](#cite-id-oO3vr8TMH04BC0en)  [\\[11\\]](#cite-id-r8eOFTRqd7j8Yu2e) \n\n## Career\n\n### Academic Career\n\nMooly Sagiv began his academic career at Tel Aviv University, where he progressed from Lecturer to Full Professor. He serves as Chair of Software Systems and Professor at the Blavatnik School of Computer Science and AI at Tel Aviv University, a position he has held since April 1998, which served as a basis for later work with [digital assets](https://iq.wiki/wiki/digital-assets).\n\nHis research has focused on program analysis and software verification. His areas of study include static program analysis, shape analysis, abstract interpretation, logic, theorem proving, programming languages, formal methods, data-flow analysis, program slicing, network verification, and smart contracts. His most cited work addresses shape analysis through three-valued logic and was implemented in the TVLA system.\n\nSagiv’s publications examine subjects such as dataflow analysis, symbolic execution, and methods used to analyze and verify program behavior. His academic work has also involved research related to theorem proving and abstract interpretation.\n\nFrom August 2006 to August 2007, Sagiv was a Visiting Professor at the University of California, Berkeley, in the Electrical Engineering and Computer Sciences (EECS) department. Between August 2008 and August 2010, he served as a Visiting Researcher at Stanford University.\n\nA study of authorship and collaborations within the Programming Languages research community referred to Sagiv as “the Kevin Bacon of the PLDI community”.\n\n### IBM\n\nSagiv worked at IBM as a Team Leader between October 1990 and October 1993 in Haifa, Israel.\n\n### Certora\n\nIn 2018, Sagiv co-founded Certora, a company focused on the formal verification of [smart contracts](https://iq.wiki/wiki/smart-contract) and blockchain-based software systems. He served as Chief Executive Officer from November 2018 until June 2025.\n\nThe company developed verification tools intended to analyze the behavior of smart contracts and software systems used in [decentralized finance](https://iq.wiki/wiki/defi) applications.\n\nIn June 2025, Sagiv assumed the role of Chief Scientist at Certora, based in the New York City Metropolitan Area.\n\nHis work at the company has involved the application of formal methods and software verification techniques to blockchain-related systems and [smart contracts](https://iq.wiki/wiki/smart-contract).\n\n### Collaborations and Professional Activities\n\nSagiv has participated in collaborative research projects related to programming languages and software engineering. His work includes collaborations involving program analysis and software verification.\n\nHe has also participated in conferences and symposiums related to computer science and software engineering, including the European Symposium on Programming (ESOP) and the International Conference on Software Engineering.\n\n### Awards and Recognition\n\nSagiv received the Wolf Foundation Fellowship in 1989 and the IBM Outstanding Technical Achievement Award in 1993. Between 2000 and 2005, he received IBM Faculty Awards.\n\nIn 2002, he received the Friedrich Wilhelm Bessel Research Award.\n\nIn 2011, Sagiv received the ACM SIGSOFT Retrospective Impact Paper Award together with Thomas Reps, Susan Horowitz, and Genevieve Rosay.\n\nIn 2016, he received the Microsoft Outstanding Collaborator Award and was named an ACM Fellow.\n\nHis work in software engineering, program analysis, and formal methods has been referenced through academic awards, research collaborations, and positions in academia and industry. [\\[1\\]](#cite-id-FgmgJZygNQOBq8qP)  [\\[2\\]](#cite-id-oO3vr8TMH04BC0en)  [\\[3\\]](#cite-id-iXCJglOBf7JbqtZI)  [\\[4\\]](#cite-id-bgyXbu14o9XEmLnd)  [\\[5\\]](#cite-id-oJg7rCGrknQ4Pw1p)  [\\[6\\]](#cite-id-p3NTtwHsu0ADUPH9)  [\\[7\\]](#cite-id-j6TEO1NDnfGSPhjq)  [\\[8\\]](#cite-id-01P3TYAt3xCDMWN0)  [\\[9\\]](#cite-id-iZ4A6WORLyAM5ndD)  [\\[10\\]](#cite-id-TJa4Awx719EMWaF9)  [\\[11\\]](#cite-id-r8eOFTRqd7j8Yu2e) ","summary":"Mooly Sagiv is an influential computer scientist known for his work in formal verification, program analysis, and smart contract security, currently serving as Chief Scientist at Certora.","images":[{"id":"QmUXX3ggHaunjc7BEha3JGTKpFAfDr2HzVWjSo51txKv8h","type":"image/jpeg, image/png"}],"categories":[{"id":"people","title":"people"}],"tags":[{"id":"Researcher"},{"id":"Developer"},{"id":"Influencer"}],"media":[{"id":"QmbSWG2FVRaqRkB5ja5sYb9SkmLeNavejdxUm8GaNrSQ6F","name":"Mooly_Sagiv.jpg","caption":"","thumbnail":"QmbSWG2FVRaqRkB5ja5sYb9SkmLeNavejdxUm8GaNrSQ6F","source":"IPFS_IMG"}],"metadata":[{"id":"references","value":"[{\"id\":\"FgmgJZygNQOBq8qP\",\"url\":\"https://www.certora.com/team\",\"description\":\"Source\",\"timestamp\":1779942116012},{\"id\":\"oO3vr8TMH04BC0en\",\"url\":\"https://www.ae-info.org/ae/Member/Sagiv\\\\_Shmuel\",\"description\":\"Academy of Europe\",\"timestamp\":1779942116012},{\"id\":\"iXCJglOBf7JbqtZI\",\"url\":\"https://en-exact-sciences.tau.ac.il/profile/msagiv\",\"description\":\"Tel Aviv University\",\"timestamp\":1779942116012},{\"id\":\"bgyXbu14o9XEmLnd\",\"url\":\"https://www2.sigsoft.org/awards/impactpaper\",\"description\":\"ACM SIGSOFT\",\"timestamp\":1779942116012},{\"id\":\"oJg7rCGrknQ4Pw1p\",\"url\":\"http://www.pl-enthusiast.net/2014/12/02/collaboration-in-pldi-oopsla/\",\"description\":\"PL Enthusiast\",\"timestamp\":1779942116012},{\"id\":\"p3NTtwHsu0ADUPH9\",\"url\":\"https://etaps.org/2023/speakers/mooly-sagiv/\",\"description\":\"ETAPS 2023\",\"timestamp\":1779942116012},{\"id\":\"j6TEO1NDnfGSPhjq\",\"url\":\"https://www.microsoft.com/en-us/research/academic-program/outstanding-collaborator-award/\",\"description\":\"Microsoft Research\",\"timestamp\":1779942116012},{\"id\":\"01P3TYAt3xCDMWN0\",\"url\":\"https://www2.sigsoft.org/awards/impactpaper/\",\"description\":\"SIGSOFT Awards\",\"timestamp\":1779942116012},{\"id\":\"iZ4A6WORLyAM5ndD\",\"url\":\"https://dblp.org/pid/s/SSagiv.html\",\"description\":\"DBLP\",\"timestamp\":1779942116012},{\"id\":\"TJa4Awx719EMWaF9\",\"url\":\"https://2014.splashcon.org/profile/moolysagiv\",\"description\":\"SPLASH 2014\",\"timestamp\":1779942116012},{\"id\":\"r8eOFTRqd7j8Yu2e\",\"description\":\"LinkedIn: Mooly Sagiv\\n\",\"timestamp\":1779942425230,\"url\":\"https://www.linkedin.com/in/mooly-sagiv-87a36010/\"}]"},{"id":"medium_profile","value":"http://www.pl-enthusiast.net/2014/12/02/collaboration-in-pldi-oopsla/"},{"id":"linkedin_profile","value":"https://www.linkedin.com/in/mooly-sagiv-87a36010/"},{"id":"commit-message","value":"\"Added Mooly Sagiv biography and people category\""}],"events":[{"id":"d84633e4-5773-459e-b409-9ec0dd092fa6","date":"2018-01-01","title":"Co-founded Certora","type":"CREATED","description":"Co-founded Certora, a company focused on scaling formal verification for smart contracts.","link":null,"continent":null,"country":null},{"id":"b1a1f017-f028-4cff-a9b1-ce277ff31533","date":"2016-01-01","title":"Became ACM Fellow","type":"DEFAULT","description":"Recognized as an ACM Fellow for contributions to software engineering and programming languages.","link":null,"continent":null,"country":null},{"id":"fd86c41c-7cbc-498f-be6f-2d4b244342e7","date":"2011-01-01","title":"Received ACM SIGSOFT Impact Paper Award","type":"DEFAULT","description":"Awarded for significant long-term impact on the field of software engineering through seminal publications.","link":null,"continent":null,"country":null},{"id":"660c06af-4650-4dc3-900b-2d0ed59f6132","date":"2005-01-01","title":"Joined Tel Aviv University as Professor","type":"DEFAULT","description":"Became a full Professor at Tel Aviv University, contributing extensively to programming languages research.","link":null,"continent":null,"country":null},{"id":"2fa93bdc-248e-46b4-9ac4-78be5d582463","date":"2002-01-01","title":"Friedrich Wilhelm Bessel Research Award","type":"DEFAULT","description":"Received the Bessel Research Award, acknowledging his influential research methods in formal verification.","link":null,"continent":null,"country":null}],"user":{"id":"0x8af7a19a26d8fbc48defb35aefb15ec8c407f889"},"author":{"id":"0x8af7a19a26d8fbc48defb35aefb15ec8c407f889"},"operator":{"id":"0xd5893989b9952c6568a99F854795AcC5Ae480D56"},"language":"en","version":1,"linkedWikis":{"blockchains":[],"founders":[],"speakers":[]}}