S. Sagiv

Most-cited papers

Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation
S. Sagiv, T. Reps, Susan Horwitz
1995Theory and Practice of Software Development354 citations Open access
Semantic Scholar
TVLA: A System for Implementing Static Analyses
T. Lev-Ami, S. Sagiv
2000Sensors Applications Symposium290 citations
Semantic Scholar
Verifying Properties of Binarized Deep Neural Networks
Nina Narodytska, S. Kasiviswanathan, L. Ryzhyk, S. Sagiv +1 more
2017AAAI Conference on Artificial Intelligence244 citations Open access
Semantic Scholar
Symbolic Implementation of the Best Transformer
T. Reps, S. Sagiv, G. Yorsh
2004International Conference on Verification, Model Checking and Abstract Interpretation181 citations
Semantic Scholar
Local Reasoning for Storable Locks and Threads
Alexey Gotsman, Josh Berdine, B. Cook, N. Rinetzky +1 more
2007Asian Symposium on Programming Languages and Systems143 citations
Semantic Scholar
Comparison Under Abstraction for Verifying Linearizability
Daphna Amit, N. Rinetzky, T. Reps, S. Sagiv +1 more
2007International Conference on Computer Aided Verification130 citations
Semantic Scholar
Proving Conditional Termination
B. Cook, Sumit Gulwani, T. Lev-Ami, A. Rybalchenko +1 more
2008International Conference on Computer Aided Verification110 citations Open access
Semantic Scholar
Verifying Reachability in Networks with Mutable Datapaths
Aurojit Panda, O. Lahav, K. Argyraki, S. Sagiv +1 more
2016Symposium on Networked Systems Design and Implementation108 citations
Semantic Scholar
Symbolically Computing Most-Precise Abstract Operations for Shape Analysis
G. Yorsh, T. Reps, S. Sagiv
2004International Conference on Tools and Algorithms for Construction and Analysis of Systems107 citations Open access
Semantic Scholar
Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists
R. Manevich, Eran Yahav, G. Ramalingam, S. Sagiv
2005International Conference on Verification, Model Checking and Abstract Interpretation105 citations
Semantic Scholar
Numeric Domains with Summarized Dimensions
Denis Gopan, F. DiMaio, Nurit Dor, T. Reps +1 more
2004International Conference on Tools and Algorithms for Construction and Analysis of Systems105 citations Open access
Semantic Scholar
Eventually Consistent Transactions
S. Burckhardt, Daan Leijen, M. Fähndrich, S. Sagiv
2012European Symposium on Programming97 citations Open access
Semantic Scholar
The Boundary Between Decidability and Undecidability for Transitive-Closure Logics
N. Immerman, A. Rabinovich, T. Reps, S. Sagiv +1 more
2004Annual Conference for Computer Science Logic93 citations
Semantic Scholar
Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures
T. Lev-Ami, N. Immerman, T. Reps, S. Sagiv +2 more
2005CADE92 citations Open access
Semantic Scholar
Cleanness Checking of String Manipulations in C Programs via Integer Analysis
Nurit Dor, M. Rodeh, S. Sagiv
2001Sensors Applications Symposium88 citations
Semantic Scholar
Interprocedural Shape Analysis for Cutpoint-Free Programs
N. Rinetzky, S. Sagiv, Eran Yahav
2005Sensors Applications Symposium86 citations
Semantic Scholar
Thread Quantification for Concurrent Shape Analysis
Josh Berdine, T. Lev-Ami, R. Manevich, G. Ramalingam +1 more
2008International Conference on Computer Aided Verification84 citations Open access
Semantic Scholar
A logic of reachable patterns in linked data-structures
G. Yorsh, A. Rabinovich, S. Sagiv, A. Meyer +1 more
2006J. Log. Algebraic Methods Program.80 citations Open access
Semantic Scholar
Interprocedural Shape Analysis for Recursive Programs
N. Rinetzky, S. Sagiv
2001International Conference on Compiler Construction78 citations
Semantic Scholar
Verifying Temporal Heap Properties Specified via Evolution Logic
Eran Yahav, T. Reps, S. Sagiv, R. Wilhelm
2003Logic Journal of the IGPL74 citations Open access
Semantic Scholar
Automatic Removal of Array Memory Leaks in Java
Ran Shaham, E. K. Kolodner, S. Sagiv
2000International Conference on Compiler Construction74 citations Open access
Semantic Scholar
Shape Analysis
R. Wilhelm, S. Sagiv, T. Reps
2000International Conference on Compiler Construction70 citations Open access
Semantic Scholar
Static Program Analysis via 3-Valued Logic
T. Reps, S. Sagiv, R. Wilhelm
2004International Conference on Computer Aided Verification69 citations Open access
Semantic Scholar
A Decidable Logic for Describing Linked Data Structures
Michael Benedikt, T. Reps, S. Sagiv
1999European Symposium on Programming69 citations Open access
Semantic Scholar
Establishing local temporal heap safety properties with applications to compile-time memory management
Ran Shaham, Eran Yahav, E. K. Kolodner, S. Sagiv
2003Science of Computer Programming68 citations Open access
Semantic Scholar
Generalizing DPLL to Richer Logics
K. McMillan, A. Kuehlmann, S. Sagiv
2009International Conference on Computer Aided Verification65 citations Open access
Semantic Scholar
Checking Cleanness in Linked Lists
Nurit Dor, M. Rodeh, S. Sagiv
2000Sensors Applications Symposium65 citations
Semantic Scholar
Revamping TVLA: Making Parametric Shape Analysis Competitive
Igor Bogudlov, T. Lev-Ami, T. Reps, S. Sagiv
2007International Conference on Computer Aided Verification63 citations
Semantic Scholar
Effectively-Propositional Reasoning about Reachability in Linked Data Structures
Shachar Itzhaky, A. Banerjee, N. Immerman, Aleksandar Nanevski +1 more
2013International Conference on Computer Aided Verification61 citations Open access
Semantic Scholar
Abstraction Refinement via Inductive Learning
Alexey Loginov, T. Reps, S. Sagiv
2005International Conference on Computer Aided Verification60 citations Open access
Semantic Scholar
Ranking Abstractions
A. Chawdhary, B. Cook, Sumit Gulwani, S. Sagiv +1 more
2008European Symposium on Programming59 citations
Semantic Scholar
Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm
Alexey Loginov, T. Reps, S. Sagiv
2006Sensors Applications Symposium55 citations
Semantic Scholar
Partially Disjunctive Heap Abstraction
R. Manevich, S. Sagiv, G. Ramalingam, J. Field
2004Sensors Applications Symposium54 citations
Semantic Scholar
Decidable Fragments of Many-Sorted Logic
Aharon Abadi, A. Rabinovich, S. Sagiv
2007Logic Programming and Automated Reasoning45 citations Open access
Semantic Scholar
Statically Inferring Complex Heap, Array, and Numeric Invariants
Bill McCloskey, T. Reps, S. Sagiv
2010Sensors Applications Symposium44 citations
Semantic Scholar
Property-Directed Shape Analysis
Shachar Itzhaky, Nikolaj S. Bjørner, T. Reps, S. Sagiv +1 more
2014International Conference on Computer Aided Verification43 citations Open access
Semantic Scholar
Core-Guided Minimal Correction Set and Core Enumeration
Nina Narodytska, Nikolaj S. Bjørner, M. Marinescu, S. Sagiv
2018International Joint Conference on Artificial Intelligence40 citations Open access
Semantic Scholar
Abstraction for Shape Analysis with Fast and Precise Transformers
T. Lev-Ami, N. Immerman, S. Sagiv
2006International Conference on Computer Aided Verification39 citations
Semantic Scholar
Automatically Verifying Concurrent Queue Algorithms
Eran Yahav, S. Sagiv
2003SoftMC@CAV38 citations Open access
Semantic Scholar
Inferring Inductive Invariants from Phase Structures
Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, S. Sagiv
2019International Conference on Computer Aided Verification37 citations Open access
Semantic Scholar
Verification via Structure Simulation
N. Immerman, A. Rabinovich, T. Reps, S. Sagiv +1 more
2004International Conference on Computer Aided Verification37 citations Open access
Semantic Scholar
A Kleene Analysis of Mobile Ambients
F. Nielson, H. R. Nielson, S. Sagiv
2000European Symposium on Programming35 citations Open access
Semantic Scholar
Heap Decomposition for Concurrent Shape Analysis
R. Manevich, T. Lev-Ami, S. Sagiv, G. Ramalingam +1 more
2008Sensors Applications Symposium34 citations
Semantic Scholar
Bounded Quantifier Instantiation for Checking Inductive Invariants
Yotam M. Y. Feldman, Oded Padon, N. Immerman, S. Sagiv +1 more
2017International Conference on Tools and Algorithms for Construction and Analysis of Systems31 citations Open access
Semantic Scholar
Verifying Isolation Properties in the Presence of Middleboxes
Aurojit Panda, O. Lahav, K. Argyraki, S. Sagiv +1 more
2014arXiv.org31 citations
Semantic Scholar
Combining Shape Analyses by Intersecting Abstractions
Gilad Arnold, R. Manevich, S. Sagiv, Ran Shaham
2006International Conference on Verification, Model Checking and Abstract Interpretation30 citations
Semantic Scholar
Compactly Representing First-Order Structures for Static Analysis
R. Manevich, G. Ramalingam, J. Field, Deepak Goyal +1 more
2002Sensors Applications Symposium29 citations
Semantic Scholar
Shape Analysis and Applications
T. Reps, S. Sagiv, R. Wilhelm
2007The Compiler Design Handbook, 2nd ed.26 citations
Semantic Scholar
TVLA: A system for generating abstract interpreters
T. Lev-Ami, R. Manevich, S. Sagiv
2004IFIP Congress Topical Sessions24 citations
Semantic Scholar
Shape Analysis by Graph Decomposition
R. Manevich, Josh Berdine, B. Cook, G. Ramalingam +1 more
2007International Conference on Tools and Algorithms for Construction and Analysis of Systems23 citations
Semantic Scholar