Mooly (Shmuel) Sagiv (born 11 April 1959,

Israel Israel (; he, יִשְׂרָאֵל, ; ar, إِسْرَائِيل, ), officially the State of Israel ( he, מְדִינַת יִשְׂרָאֵל, label=none, translit=Medīnat Yīsrāʾēl; ), is a country in Western Asia. It is situated ...

) is an Israeli

computer scientist A computer scientist is a person who is trained in the academic study of computer science. Computer scientists typically work on the theoretical side of computation, as opposed to the hardware side on which computer engineers mainly focus (al ...

known for his work on

static program analysis In computer science, static program analysis (or static analysis) is the analysis of computer programs performed without executing them, in contrast with dynamic program analysis, which is performed on programs during their execution. The term i ...

. He is currently Chair of Software Systems in the School of Computer Science at

Tel Aviv University Tel Aviv University (TAU) ( he, אוּנִיבֶרְסִיטַת תֵּל אָבִיב, ''Universitat Tel Aviv'') is a public research university in Tel Aviv, Israel. With over 30,000 students, it is the largest university in the country. Locate ...

, and CEO of Certora, a

startup company A startup or start-up is a company or project undertaken by an entrepreneur to seek, develop, and validate a scalable business model. While entrepreneurship refers to all new businesses, including self-employment and businesses that never intend t ...

providing

formal verification 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 metho ...

smart contract A smart contract is a computer program or a transaction protocol that is intended to automatically execute, control or document events and actions according to the terms of a contract or an agreement. The objectives of smart contracts are the re ...

s. Sagiv's research spans areas including static

program analysis In computer science, program analysis is the process of automatically analyzing the behavior of computer programs regarding a property such as correctness, robustness, safety and liveness. Program analysis focuses on two major areas: program op ...

, shape analysis,

abstract interpretation In computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a partial execution of a computer prog ...

logic Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises ...

theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a maj ...

programming language A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming ...

formal methods In computer science, formal methods are mathematically rigorous techniques 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 expec ...

data-flow analysis In computing, dataflow is a broad concept, which has various meanings depending on the application and context. In the context of software architecture, data flow relates to stream processing or reactive programming. Software architecture Dataf ...

program slicing In computer programming, program slicing is the computation of the set of program statements, the program slice, that may affect the values at some point of interest, referred to as a slicing criterion. Program slicing can be used in debugging t ...

, network verification, and

s. His most cited work is on shape analysis via three-valued logic, implemented in the TVLA system. For his work, Sagiv was awarded the

Wolf Foundation The Wolf Foundation is a private not-for-profit organization in Israel established in 1975 by Ricardo Wolf, a German-born Jewish Cuban inventor and former Cuban ambassador to Israel. Ricardo Wolf Ricardo Wolf, the founder of the Wolf Foundat ...

Fellowship (1989), IBM Outstanding Technical Achievement Award (1993), Friedrich Wilhelm Bessel Research Award (2002), IBM Faculty Awards (2000-2005), Chair of Software Systems in the School of Computer Science, Tel Aviv University (2008), ACM SIGSOFT Retrospective Impact Paper Award (with Thomas Reps, Susan Horowitz, and Genevieve Rosay, 2011), Microsoft Outstanding Collaborator Award (2016), and

ACM Fellow ACM or A.C.M. may refer to: Aviation * AGM-129 ACM, 1990–2012 USAF cruise missile * Air chief marshal * Air combat manoeuvring or dogfighting * Air cycle machine * Arica Airport (Colombia) (IATA: ACM), in Arica, Amazonas, Colombia Computing ...

(2016). An analysis of authorship and collaborations in the Programming Languages research community has called Sagiv "the

Kevin Bacon Kevin Norwood Bacon (born July 8, 1958) is an American actor. His films include the musical-drama film '' Footloose'' (1984), the controversial historical conspiracy legal thriller '' JFK'' (1991), the legal drama '' A Few Good Men'' (1992), t ...

of the

PLDI Programming Language Design and Implementation (PLDI) is one of the ACM SIGPLAN's most important conferences. The precursor of PLDI was the Symposium on Compiler Optimization, held July 27–28, 1970 at the University of Illinois at Urbana-Ch ...

community". Sagiv is married to Dr. Tamar Sagiv, and together they have three daughters. Aya Sagiv, Naama Sagiv, and Hagar Sagiv.

References

External links

TVLA websiteIVy projectCertora website
{{DEFAULTSORT:Sagiv, Shmuel Israeli computer scientists Academic staff of Tel Aviv University Technion – Israel Institute of Technology alumni 1959 births Living people