Shmuel Sagiv - Selected Publications#

Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, Sharon Shoham: Complexity and information in invariant inference. Proc. ACM Program. Lang. 4(POPL): 5:1-5:29 (2020)

Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk, Mooly Sagiv: Simple and precise static analysis of untrusted Linux kernel extensions. PLDI 2019: 1069-1084. The results are used by Microsoft to ensure security.

Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, Yoni Zohar: Online detection of effectively callback free objects with applications to smart contracts. Proc. ACM Program. Lang. 2(POPL): 48:1-48:28 (2018). 110 Citations. This article is the basis of the Certora company, www.certora.com

Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham: Ivy: safety verification by interactive generalization. PLDI 2016: 614-630

This article started a series of theoretical results by Oded published at POPL’16, OOPSLA’17, POPL’18, PLDI’18 and implemented in an open source system by Microsoft called Ivy which is used by companies and universities. The results appear in the PhD dissertation of Oded Padon which received the ETAPS Doctoral Dissertation Award 2020

Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv: Effectively-Propositional Reasoning about Reachability in Linked Data Structures. CAV 2013: 756-772. This article started the PhD dissertation of Shachar Itzhaky (Now a faculty member at Technion) which won the Sigplan Dissertation award

Ohad Shacham, Nathan Grasso Bronson, Alex Aiken, Mooly Sagiv, Martin T. Vechev, Eran Yahav: Testing atomicity of composed concurrent operations. OOPSLA 2011: 51-64. This article changed the design of the Java concurrent library

Peter Hawkins, Martin C. Rinard, Alex Aiken, Mooly Sagiv, Kathleen Fisher: An introduction to data representation synthesis. Commun. ACM 55(12): 91-99 (2012). The PHD thesis of Peter Hawkins won an honorary mention in the ACM dissertation award and two best paper awards in PLDI’11 and PLDI’12.

Mooly Sagiv, Thomas W. Reps, Reinhard Wilhelm: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3): 217-298 (2002) 1357 Citations, the basis for the works in shape analysis also implemented in TVLA

Thomas W. Reps, Susan Horwitz, Shmuel Sagiv: Precise Interprocedural Dataflow Analysis via Graph Reachability. POPL 1995: 49-61 1271 Citations. This article defines the interprocedural algorithm implemented in Microsoft Static Driver Verification used to verify the correctness of device drivers.14-630