Shmuel Sagiv

According to our database, Shmuel Sagiv authored at least 173 papers between 1989 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2023

Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols.

Orr Tamir, Marcelo Taube, Kenneth L. McMillan, Sharon Shoham, Jon Howell, Guy Gueta, Mooly Sagiv

Proc. ACM Program. Lang., October, 2023

Relaxed Effective Callback Freedom: A Parametric Correctness Condition for Sequential Modules With Callbacks.

Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodríguez-Núñez, Albert Rubio, Mooly Sagiv

IEEE Trans. Dependable Secur. Comput., 2023

2022

Property-directed reachability as abstract interpretation in the monotone theory.

Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox

Proc. ACM Program. Lang., 2022

This is not the End: Rethinking Serverless Function Termination.

Kalev Alpernas, Aurojit Panda, Mooly Sagiv

CoRR, 2022

Blockaid: Data Access Policy Enforcement for Web Applications.

Wen Zhang, Eric Sheng, Michael Alan Chang, Aurojit Panda, Mooly Sagiv, Scott Shenker

Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation, 2022

2021

Learning the boundary of inductive invariants.

Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox

Proc. ACM Program. Lang., 2021

Temporal prophecy for proving temporal properties of infinite-state systems.

Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham

Formal Methods Syst. Des., 2021

Phoenix: A Formally Verified Regenerating Vault.

Uri Kirstein, Shelly Grossman, Michael Mirkin, James Wilcox, Ittay Eyal, Mooly Sagiv

CoRR, 2021

Cloud-Scale Runtime Verification of Serverless Applications.

Kalev Alpernas, Aurojit Panda, Leonid Ryzhyk, Mooly Sagiv

Proceedings of the SoCC '21: ACM Symposium on Cloud Computing, 2021

Summing up Smart Transitions.

Neta Elad, Sophie Rain, Neil Immerman, Laura Kovács, Mooly Sagiv

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020

Complexity and information in invariant inference.

Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, Sharon Shoham

Proc. ACM Program. Lang., 2020

Taming callbacks for smart contract modularity.

Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodríguez-Núñez, Albert Rubio, Mooly Sagiv

Proc. ACM Program. Lang., 2020

Invited Talk: Harnessing SMT Solvers for Verifying Low Level Programs.

Mooly Sagiv

Proceedings of the 18th International Workshop on Satisfiability Modulo Theories co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), 2020

2019

Bounded Quantifier Instantiation for Checking Inductive Invariants.

Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham

Log. Methods Comput. Sci., 2019

Some complexity results for stateful network verification.

Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner

Formal Methods Syst. Des., 2019

Automating Cluster Management with Weave.

Lalith Suresh, João Loff, Faria Kalim, Nina Narodytska, Leonid Ryzhyk, Sahan Gamage, Brian Oki, Zeeshan Lokhandwala, Mukesh Hira, Mooly Sagiv

CoRR, 2019

Simple and precise static analysis of untrusted Linux kernel extensions.

Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk, Mooly Sagiv

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Synthesizing Cluster Management Code for Distributed Systems.

Lalith Suresh, João Loff, Nina Narodytska, Leonid Ryzhyk, Mooly Sagiv, Brian Oki

Proceedings of the Workshop on Hot Topics in Operating Systems, 2019

Inferring Inductive Invariants from Phase Structures.

Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018

Reducing liveness to safety in first-order logic.

Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham

Proc. ACM Program. Lang., 2018

Online detection of effectively callback free objects with applications to smart contracts.

Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, Yoni Zohar

Proc. ACM Program. Lang., 2018

Secure serverless computing using dynamic information flow control.

Kalev Alpernas, Cormac Flanagan, Sadjad Fouladi, Leonid Ryzhyk, Mooly Sagiv, Thomas Schmitz, Keith Winstein

Proc. ACM Program. Lang., 2018

Constrained Image Generation Using Binarized Neural Networks with Decision Procedures.

Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj S. Bjørner, Mooly Sagiv

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2018, 2018

Abstract Interpretation of Stateful Networks.

Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner

Proceedings of the Static Analysis - 25th International Symposium, 2018

Modularity for decidability of deductive verification with applications to distributed systems.

Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, Doug Woos

Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Core-Guided Minimal Correction Set and Core Enumeration.

Nina Narodytska, Nikolaj S. Bjørner, Maria-Cristina V. Marinescu, Mooly Sagiv

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, 2018

Verifying Properties of Binarized Deep Neural Networks.

Nina Narodytska, Shiva Prasad Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, Toby Walsh

Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, 2018

2017

Automatic Scalable Atomicity via Semantic Locking.

Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv, Eran Yahav

ACM Trans. Parallel Comput., 2017

Synthesis of circular compositional program proofs via abduction.

Isil Dillig, Thomas Dillig, Boyang Li, Kenneth L. McMillan, Mooly Sagiv

Int. J. Softw. Tools Technol. Transf., 2017

Paxos made EPR: decidable reasoning about distributed protocols.

Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham

Proc. ACM Program. Lang., 2017

Modular Safety Verification for Stateful Networks.

Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner

CoRR, 2017

Conjunctive Abstract Interpretation Using Paramodulation.

Or Ozeri, Oded Padon, Noam Rinetzky, Mooly Sagiv

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

Property Directed Reachability for Proving Absence of Concurrent Modification Errors.

Asya Frumkin, Yotam M. Y. Feldman, Ondrej Lhoták, Oded Padon, Mooly Sagiv, Sharon Shoham

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

Verifying Reachability in Networks with Mutable Datapaths.

Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker

Proceedings of the 14th USENIX Symposium on Networked Systems Design and Implementation, 2017

On the Automated Verification of Web Applications with Embedded SQL.

Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, Florian Zuleger

Proceedings of the 20th International Conference on Database Theory, 2017

Verification in the Age of Microservices.

Aurojit Panda, Mooly Sagiv, Scott Shenker

Proceedings of the 16th Workshop on Hot Topics in Operating Systems, 2017

Abduction for Learning Smart City Rules.

Nikolaj S. Bjørner, Maria-Cristina V. Marinescu, Mooly Sagiv

Proceedings of the GCAI 2017, 2017

Verifying Equivalence of Spark Programs.

Shelly Grossman, Sara Cohen, Shachar Itzhaky, Noam Rinetzky, Mooly Sagiv

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2016

Decidability of inferring inductive invariants.

Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Ivy: safety verification by interactive generalization.

Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham

Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

Simple Invariants for Proving the Safety of Distributed Protocols (Invited Talk).

Mooly Sagiv

Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2016

2015

New Directions for Network Verification.

Aurojit Panda, Katerina J. Argyraki, Mooly Sagiv, Michael Schapira, Scott Shenker

Proceedings of the 1st Summit on Advances in Programming Languages, 2015

Modularity in Lattices: A Case Study on the Correspondence Between Top-Down and Bottom-Up Analysis.

Ghila Castelnuovo, Mayur Naik, Noam Rinetzky, Mooly Sagiv, Hongseok Yang

Proceedings of the Static Analysis - 22nd International Symposium, 2015

Decentralizing SDN Policies.

Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Composing concurrency control.

Ofri Ziv, Alex Aiken, Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

2014

Verifying Isolation Properties in the Presence of Middleboxes.

Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker

CoRR, 2014

Automatic semantic locking.

Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv, Eran Yahav

Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2014

Modular reasoning about heap paths via effectively propositional formulas.

Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

VeriCon: towards verifying controller programs in software-defined networks.

Thomas Ball, Nikolaj S. Bjørner, Aaron Gember, Shachar Itzhaky, Aleksandr Karbyshev, Mooly Sagiv, Michael Schapira, Asaf Valadarsky

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014

Verifying atomicity via data independence.

Ohad Shacham, Eran Yahav, Guy Golan-Gueta, Alex Aiken, Nathan Grasso Bronson, Mooly Sagiv, Martin T. Vechev

Proceedings of the International Symposium on Software Testing and Analysis, 2014

Checking Linearizability of Encapsulated Extended Operations.

Oren Zomer, Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv

Proceedings of the Programming Languages and Systems, 2014

Property-Directed Shape Analysis.

Shachar Itzhaky, Nikolaj S. Bjørner, Thomas W. Reps, Mooly Sagiv, Aditya V. Thakur

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013

Principles of POPL.

Derek Dreyer, John Field, Roberto Giacobazzi, Michael Hicks, Suresh Jagannathan, Mooly Sagiv, Peter Sewell, Philip Wadler

ACM SIGPLAN Notices, 2013

Concurrent libraries with foresight.

Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv, Eran Yahav

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013

Turning nondeterminism into parallelism.

Omer Tripp, Eric Koskinen, Mooly Sagiv

Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, 2013

Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning.

Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Effectively-Propositional Reasoning about Reachability in Linked Data Structures.

Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs.

Jörg Kreiker, Thomas W. Reps, Noam Rinetzky, Mooly Sagiv, Reinhard Wilhelm, Eran Yahav

Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

2012

POPL'11 program chair's report.

Mooly Sagiv

ACM SIGPLAN Notices, 2012

An introduction to data representation synthesis.

Peter Hawkins, Martin C. Rinard, Alex Aiken, Mooly Sagiv, Kathleen Fisher

Commun. ACM, 2012

Abstractions from tests.

Mayur Naik, Hongseok Yang, Ghila Castelnuovo, Mooly Sagiv

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

JANUS: exploiting parallelism via hindsight.

Omer Tripp, Roman Manevich, John Field, Mooly Sagiv

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2012

Concurrent data representation synthesis.

Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2012

Understanding the behavior of database operations under program control.

Juan M. Tamayo, Alex Aiken, Nathan Grasso Bronson, Mooly Sagiv

Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2012

Reasoning about Lock Placements.

Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv

Proceedings of the Programming Languages and Systems, 2012

Eventually Consistent Transactions.

Sebastian Burckhardt, Daan Leijen, Manuel Fähndrich, Mooly Sagiv

Proceedings of the Programming Languages and Systems, 2012

2011

Data representation synthesis.

Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv

Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011

Precise and compact modular procedure summaries for heap manipulating programs.

Isil Dillig, Thomas Dillig, Alex Aiken, Mooly Sagiv

Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011

HAWKEYE: effective discovery of dataflow impediments to parallelization.

Omer Tripp, Greta Yorsh, John Field, Mooly Sagiv

Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2011

Testing atomicity of composed concurrent operations.

Ohad Shacham, Nathan Grasso Bronson, Alex Aiken, Mooly Sagiv, Martin T. Vechev, Eran Yahav

Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2011

Automatic fine-grain locking using shape properties.

Guy Golan-Gueta, Nathan Grasso Bronson, Alex Aiken, G. Ramalingam, Mooly Sagiv, Eran Yahav

Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2011

2010

Verifying safety properties of concurrent heap-manipulating programs.

Eran Yahav, Mooly Sagiv

ACM Trans. Program. Lang. Syst., 2010

Finite differencing of logical formulas for static analysis.

Thomas W. Reps, Mooly Sagiv, Alexey Loginov

ACM Trans. Program. Lang. Syst., 2010

A relational approach to interprocedural shape analysis.

Bertrand Jeannet, Alexey Loginov, Thomas W. Reps, Mooly Sagiv

ACM Trans. Program. Lang. Syst., 2010

Decidable fragments of many-sorted logic.

Aharon Abadi, Alexander Rabinovich, Mooly Sagiv

J. Symb. Comput., 2010

Field-sensitive program dependence analysis.

Shay Litvak, Nurit Dor, Rastislav Bodík, Noam Rinetzky, Mooly Sagiv

Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010

Statically Inferring Complex Heap, Array, and Numeric Invariants.

Bill McCloskey, Thomas W. Reps, Mooly Sagiv

Proceedings of the Static Analysis - 17th International Symposium, 2010

A dynamic evaluation of the precision of static heap abstractions.

Percy Liang, Omer Tripp, Mayur Naik, Mooly Sagiv

Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2010

A simple inductive synthesis methodology and its applications.

Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv

Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2010

Specifying and verifying sparse matrix codes.

Gilad Arnold, Johannes Hölzl, Ali Sinan Köksal, Rastislav Bodík, Mooly Sagiv

Proceedings of the Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, 2010

Data Structure Fusion.

Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv

Proceedings of the Programming Languages and Systems - 8th Asian Symposium, 2010

2009

Self-stabilization preserving compiler.

Shlomi Dolev, Yinnon A. Haviv, Mooly Sagiv

ACM Trans. Program. Lang. Syst., 2009

Simulating reachability using first-order logic with applications to verification of linked data structures

Tal Lev-Ami, Neil Immerman, Thomas W. Reps, Mooly Sagiv, Siddharth Srivastava, Greta Yorsh

Log. Methods Comput. Sci., 2009

Thread-Modular Shape Analysis.

Mooly Sagiv

Proceedings of the Verification, 2009

A combination framework for tracking partition sizes.

Sumit Gulwani, Tal Lev-Ami, Mooly Sagiv

Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

09301 Executive Summary - Typing, Analysis, and Verification of Heap-Manipulating Programs.

Mooly Sagiv, Arnd Poetzsch-Heffter, Peter W. O'Hearn

Proceedings of the Typing, Analysis and Verification of Heap-Manipulating Programs, 19.07., 2009

09301 Abstracts Collection - Typing, Analysis, and Verification of Heap-Manipulating Programs.

Mooly Sagiv, Arnd Poetzsch-Heffter, Peter W. O'Hearn

Proceedings of the Typing, Analysis and Verification of Heap-Manipulating Programs, 19.07., 2009

Generalizing DPLL to Richer Logics.

Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

Abstract Transformers for Thread Correlation Analysis.

Michal Segalov, Tal Lev-Ami, Roman Manevich, Ganesan Ramalingam, Mooly Sagiv

Proceedings of the Programming Languages and Systems, 7th Asian Symposium, 2009

2008

On the complexity of partially-flow-sensitive alias analysis.

Noam Rinetzky, G. Ramalingam, Shmuel Sagiv, Eran Yahav

ACM Trans. Program. Lang. Syst., 2008

Heap Decomposition for Concurrent Shape Analysis.

Roman Manevich, Tal Lev-Ami, Mooly Sagiv, Ganesan Ramalingam, Josh Berdine

Proceedings of the Static Analysis, 15th International Symposium, 2008

Customization change impact analysis for erp professionals via program slicing.

Nurit Dor, Tal Lev-Ami, Shay Litvak, Mooly Sagiv, Dror Weiss

Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, 2008

Ranking Abstractions.

Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, Hongseok Yang

Proceedings of the Programming Languages and Systems, 2008

Proving Conditional Termination.

Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

Thread Quantification for Concurrent Shape Analysis.

Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, Shmuel Sagiv

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007

Introduction to special ESOP'05 issue.

Mooly Sagiv

ACM Trans. Program. Lang. Syst., 2007

Logical characterizations of heap abstractions.

Greta Yorsh, Thomas W. Reps, Mooly Sagiv, Reinhard Wilhelm

ACM Trans. Comput. Log., 2007

Scaling model checking of dataraces using dynamic information.

Ohad Shacham, Mooly Sagiv, Assaf Schuster

J. Parallel Distributed Comput., 2007

A logic of reachable patterns in linked data-structures.

Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani

J. Log. Algebraic Methods Program., 2007

Constructing Specialized Shape Analyses for Uniform Change.

Tal Lev-Ami, Mooly Sagiv, Neil Immerman, Thomas W. Reps

Proceedings of the Verification, 2007

Shape Analysis by Graph Decomposition.

Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Cartesian Partial-Order Reduction.

Guy Gueta, Cormac Flanagan, Eran Yahav, Mooly Sagiv

Proceedings of the Model Checking Software, 2007

Thread-modular shape analysis.

Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv

Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

Modular Shape Analysis for Dynamically Encapsulated Programs.

Noam Rinetzky, Arnd Poetzsch-Heffter, Ganesan Ramalingam, Mooly Sagiv, Eran Yahav

Proceedings of the Programming Languages and Systems, 2007

Revamping TVLA: Making Parametric Shape Analysis Competitive.

Igor Bogudlov, Tal Lev-Ami, Thomas W. Reps, Mooly Sagiv

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Leaping Loops in the Presence of Abstraction.

Thomas Ball, Orna Kupferman, Mooly Sagiv

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Comparison Under Abstraction for Verifying Linearizability.

Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, Eran Yahav

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Labelled Clauses.

Tal Lev-Ami, Christoph Weidenbach, Thomas W. Reps, Mooly Sagiv

Proceedings of the Automated Deduction, 2007

Local Reasoning for Storable Locks and Threads.

Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv

Proceedings of the Programming Languages and Systems, 5th Asian Symposium, 2007

Shape Analysis and Applications.

Thomas W. Reps, Mooly Sagiv, Reinhard Wilhelm

Proceedings of the Compiler Design Handbook: Optimizations and Machine Code Generation, 2007

2006

Install-Time Vaccination of Windows Executables to Defend against Stack Smashing Attacks.

Danny Nebenzahl, Shmuel Sagiv, Avishai Wool

IEEE Trans. Dependable Secur. Comput., 2006

Verifying Temporal Heap Properties Specified via Evolution Logic.

Eran Yahav, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm

Log. J. IGPL, 2006

Combining Shape Analyses by Intersecting Abstractions.

Gilad Arnold, Roman Manevich, Mooly Sagiv, Ran Shaham

Proceedings of the Verification, 2006

Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm.

Alexey Loginov, Thomas W. Reps, Mooly Sagiv

Proceedings of the Static Analysis, 13th International Symposium, 2006

Testing, abstraction, theorem proving: better together!

Greta Yorsh, Thomas Ball, Mooly Sagiv

Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, 2006

Abstraction for Shape Analysis with Fast and Precise Transformers.

Tal Lev-Ami, Neil Immerman, Shmuel Sagiv

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

An Appreciation of the Work of Reinhard Wilhelm.

Thomas W. Reps, Mooly Sagiv, Jörg Bauer

Proceedings of the Program Analysis and Compilation, 2006

Abstract Counterexample-Based Refinement for Powerset Domains.

Roman Manevich, John Field, Thomas A. Henzinger, G. Ramalingam, Mooly Sagiv

Proceedings of the Program Analysis and Compilation, 2006

Refinement-Based Verification for Possibly-Cyclic Lists.

Alexey Loginov, Thomas W. Reps, Mooly Sagiv

Proceedings of the Program Analysis and Compilation, 2006

2005

Establishing local temporal heap safety properties with applications to compile-time memory management.

Ran Shaham, Eran Yahav, Elliot K. Kolodner, Mooly Sagiv

Sci. Comput. Program., 2005

Automatic Assume/Guarantee Reasoning for Heap-Manipulating Programs: Ongoing Work.

Greta Yorsh, Alexey Skidanov, Thomas W. Reps, Shmuel Sagiv

Proceedings of the First International Workshop on Abstract Interpretation of Object-oriented Languages, 2005

Automatic Verification of Strongly Dynamic Software Systems.

Nurit Dor, John Field, Denis Gopan, Tal Lev-Ami, Alexey Loginov, Roman Manevich, G. Ramalingam, Thomas W. Reps, Noam Rinetzky, Mooly Sagiv, Reinhard Wilhelm, Eran Yahav, Greta Yorsh

Proceedings of the Verified Software: Theories, 2005

Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists.

Roman Manevich, Eran Yahav, Ganesan Ramalingam, Shmuel Sagiv

Proceedings of the Verification, 2005

Interprocedural Shape Analysis for Cutpoint-Free Programs.

Noam Rinetzky, Mooly Sagiv, Eran Yahav

Proceedings of the Static Analysis, 12th International Symposium, 2005

A semantics for procedure local heaps and its abstractions.

Noam Rinetzky, Jörg Bauer, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm

Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005

A framework for numeric analysis of array operations.

Denis Gopan, Thomas W. Reps, Shmuel Sagiv

Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005

Optimizing C Multithreaded Memory Management Using Thread-Local Storage.

Yair Sade, Shmuel Sagiv, Ran Shaham

Proceedings of the Compiler Construction, 14th International Conference, 2005

Abstraction Refinement via Inductive Learning.

Alexey Loginov, Thomas W. Reps, Shmuel Sagiv

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004

On the Expressive Power of Canonical Abstraction.

Shmuel Sagiv

Proceedings of the Verification, 2004

Symbolic Implementation of the Best Transformer.

Thomas W. Reps, Shmuel Sagiv, Greta Yorsh

Proceedings of the Verification, 2004

Symbolically Computing Most-Precise Abstract Operations for Shape Analysis.

Greta Yorsh, Thomas W. Reps, Shmuel Sagiv

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Numeric Domains with Summarized Dimensions.

Denis Gopan, Frank DiMaio, Nurit Dor, Thomas W. Reps, Shmuel Sagiv

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Partially Disjunctive Heap Abstraction.

Roman Manevich, Shmuel Sagiv, Ganesan Ramalingam, John Field

Proceedings of the Static Analysis, 11th International Symposium, 2004

TVLA: A system for generating abstract interpreters.

Tal Lev-Ami, Roman Manevich, Shmuel Sagiv

Proceedings of the Building the Information Society, 2004

The Boundary Between Decidability and Undecidability for Transitive-Closure Logics.

Neil Immerman, Alexander Moshe Rabinovich, Thomas W. Reps, Shmuel Sagiv, Greta Yorsh

Proceedings of the Computer Science Logic, 18th International Workshop, 2004

Static Program Analysis via 3-Valued Logic.

Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Verification via Structure Simulation.

Neil Immerman, Alexander Moshe Rabinovich, Thomas W. Reps, Shmuel Sagiv, Greta Yorsh

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003

Automatically Verifying Concurrent Queue Algorithms.

Eran Yahav, Shmuel Sagiv

Proceedings of the 2003 Workshop on Software Model Checking, 2003

CSSV: towards a realistic tool for statically detecting all buffer overflows in C.

Nurit Dor, Michael Rodeh, Shmuel Sagiv

Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003, 2003

2002

Parametric shape analysis via 3-valued logic.

Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm

ACM Trans. Program. Lang. Syst., 2002

Compactly Representing First-Order Structures for Static Analysis.

Roman Manevich, G. Ramalingam, John Field, Deepak Goyal, Shmuel Sagiv

Proceedings of the Static Analysis, 9th International Symposium, 2002

Deriving Specialized Program Analyses for Certifying Component-Client Conformance.

G. Ramalingam, Alex Varshavsky, John Field, Deepak Goyal, Shmuel Sagiv

Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2002

Semantic Minimization of 3-Valued Propositional Formulae.

Thomas W. Reps, Alexey Loginov, Shmuel Sagiv

Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 2002

Estimating the impact of heap liveness information on space consumption in Java.

Ran Shaham, Elliot K. Kolodner, Shmuel Sagiv

Proceedings of The Workshop on Memory Systems Performance (MSP 2002), 2002

Online Subpath Profiling.

David Oren, Yossi Matias, Shmuel Sagiv

Proceedings of the Compiler Construction, 11th International Conference, 2002

Shape Analysis and Applications.

Reinhard Wilhelm, Thomas W. Reps, Shmuel Sagiv

Proceedings of the Compiler Design Handbook: Optimizations and Machine Code Generation, 2002

2001

Kleene's Logic with Equality.

Flemming Nielson, Hanne Riis Nielson, Shmuel Sagiv

Inf. Process. Lett., 2001

Cleanness Checking of String Manipulations in C Programs via Integer Analysis.

Nurit Dor, Michael Rodeh, Shmuel Sagiv

Proceedings of the Static Analysis, 8th International Symposium, 2001

Heap Profiling for Space-Efficient Java.

Ran Shaham, Elliot K. Kolodner, Shmuel Sagiv

Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2001

Interprocedural Shape Analysis for Recursive Programs.

Noam Rinetzky, Shmuel Sagiv

Proceedings of the Compiler Construction, 10th International Conference, 2001

2000

TVLA: A System for Implementing Static Analyses.

Tal Lev-Ami, Shmuel Sagiv

Proceedings of the Static Analysis, 7th International Symposium, 2000

Checking Cleanness in Linked Lists.

Nurit Dor, Michael Rodeh, Shmuel Sagiv

Proceedings of the Static Analysis, 7th International Symposium, 2000

On the Effectiveness of GC in Java.

Ran Shaham, Elliot K. Kolodner, Shmuel Sagiv

Proceedings of the ISMM 2000, 2000

Putting static analysis to work for verification: A case study.

Tal Lev-Ami, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm

Proceedings of the International Symposium on Software Testing and Analysis, 2000

A Kleene Analysis of Mobile Ambients.

Flemming Nielson, Hanne Riis Nielson, Shmuel Sagiv

Proceedings of the Programming Languages and Systems, 2000

Shape Analysis.

Reinhard Wilhelm, Shmuel Sagiv, Thomas W. Reps

Proceedings of the Compiler Construction, 9th International Conference, 2000

Automatic Removal of Array Memory Leaks in Java.

Ran Shaham, Elliot K. Kolodner, Shmuel Sagiv

Proceedings of the Compiler Construction, 9th International Conference, 2000

1999

Finding Circular Attributes in Attribute Grammars.

Michael Rodeh, Shmuel Sagiv

J. ACM, 1999

A Decidable Logic for Describing Linked Data Structures.

Michael Benedikt, Thomas W. Reps, Shmuel Sagiv

Proceedings of the Programming Languages and Systems, 1999

1998

Solving Shape-Analysis Problems in Languages with Destructive Updating.

Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm

ACM Trans. Program. Lang. Syst., 1998

Building a Bridge between Pointer Aliases and Program Dependences.

John L. Ross, Shmuel Sagiv

Nord. J. Comput., 1998

A Logic-Based Approach to Program Flow Analysis.

Shmuel Sagiv, Nissim Francez, Michael Rodeh, Reinhard Wilhelm

Acta Informatica, 1998

Edge Profiling versus Path Profiling: The Showdown.

Thomas Ball, Peter Mataga, Shmuel Sagiv

Proceedings of the POPL '98, 1998

Detecting Memory Errors via Static Pointer Analysis (Preliminary Experience).

Nurit Dor, Michael Rodeh, Shmuel Sagiv

Proceedings of the SIGPLAN/SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, 1998

1996

Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation.

Shmuel Sagiv, Thomas W. Reps, Susan Horwitz

Theor. Comput. Sci., 1996

1995

Demand Interprocedural Dataflow Analysis.

Susan Horwitz, Thomas W. Reps, Shmuel Sagiv

Proceedings of the Third ACM SIGSOFT Symposium on Foundations of Software Engineering, 1995

Precise Interprocedural Dataflow Analysis via Graph Reachability.

Thomas W. Reps, Susan Horwitz, Shmuel Sagiv

Proceedings of the Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1995

1994

Speeding up Slicing.

Thomas W. Reps, Susan Horwitz, Shmuel Sagiv, Genevieve Rosay

Proceedings of the Second ACM SIGSOFT Symposium on Foundations of Software Engineering, 1994

1992

The Expressive Power of Side Effects in Prolog.

Johann A. Makowsky, J.-C. Gregoire, Shmuel Sagiv

J. Log. Program., 1992

Proving Safety of Speculative Load Instructions at Compile Time.

David Bernstein, Michael Rodeh, Shmuel Sagiv

Proceedings of the ESOP '92, 1992

1991

High level formalisms for program flow analysis and their use in compiling.

Shmuel Sagiv

PhD thesis, 1991

1990

A Logic-Based Approach to Data Flow Analysis Problem.

Shmuel Sagiv, Nissim Francez, Michael Rodeh, Reinhard Wilhelm

Proceedings of the Programming Language Implementation and Logic Programming, 1990

1989

Resolving Circularity in Attribute Grammars with Applications to Data Flow Analysis.

Shmuel Sagiv, Orit Edelstein, Nissim Francez, Michael Rodeh

Proceedings of the Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, 1989