Resolving Circularity in Attribute Grammars with Applications to Data Flow Analysis. - Shmuel Sagiv; Orit Edelstein; Nissim Francez; Michael Rodeh (POPL, 1989)

A Logic-Based Approach to Data Flow Analysis Problem. - Shmuel Sagiv; Nissim Francez; Michael Rodeh; Reinhard Wilhelm (PLILP, 1990)

High level formalisms for program flow analysis and their use in compiling. - Shmuel Sagiv (1991)

Proving Safety of Speculative Load Instructions at Compile Time. - David Bernstein; Michael Rodeh; Shmuel Sagiv (ESOP, 1992)

The Expressive Power of Side Effects in Prolog. - Johann A. Makowsky; J.-C. Gregoire; Shmuel Sagiv (J. Log. Program., 1992)

Speeding up Slicing. - Thomas W. Reps; Susan Horwitz; Shmuel Sagiv; Genevieve Rosay (SIGSOFT FSE, 1994)

Precise Interprocedural Dataflow Analysis via Graph Reachability. - Thomas W. Reps; Susan Horwitz; Shmuel Sagiv (POPL, 1995)

Demand Interprocedural Dataflow Analysis. - Susan Horwitz; Thomas W. Reps; Shmuel Sagiv (SIGSOFT FSE, 1995)

Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation. - Shmuel Sagiv; Thomas W. Reps; Susan Horwitz (Theor. Comput. Sci., 1996)

Detecting Memory Errors via Static Pointer Analysis (Preliminary Experience). - Nurit Dor; Michael Rodeh; Shmuel Sagiv (PASTE, 1998)

Edge Profiling versus Path Profiling: The Showdown. - Thomas Ball 001; Peter Mataga; Shmuel Sagiv (POPL, 1998)

A Logic-Based Approach to Program Flow Analysis. - Shmuel Sagiv; Nissim Francez; Michael Rodeh; Reinhard Wilhelm (Acta Informatica, 1998)

Building a Bridge between Pointer Aliases and Program Dependences. - John L. Ross; Shmuel Sagiv (Nord. J. Comput., 1998)

Solving Shape-Analysis Problems in Languages with Destructive Updating. - Shmuel Sagiv; Thomas W. Reps; Reinhard Wilhelm (ACM Trans. Program. Lang. Syst., 1998)

A Decidable Logic for Describing Linked Data Structures. - Michael Benedikt; Thomas W. Reps; Shmuel Sagiv (ESOP, 1999)

Finding Circular Attributes in Attribute Grammars. - Michael Rodeh; Shmuel Sagiv (J. ACM, 1999)

Automatic Removal of Array Memory Leaks in Java. - Ran Shaham; Elliot K. Kolodner; Shmuel Sagiv (CC, 2000)

Shape Analysis. - Reinhard Wilhelm; Shmuel Sagiv; Thomas W. Reps (CC, 2000)

A Kleene Analysis of Mobile Ambients. - Flemming Nielson; Hanne Riis Nielson; Shmuel Sagiv (ESOP, 2000)

Putting static analysis to work for verification: A case study. - Tal Lev-Ami; Thomas W. Reps; Shmuel Sagiv; Reinhard Wilhelm (ISSTA, 2000)

On the Effectiveness of GC in Java. - Ran Shaham; Elliot K. Kolodner; Shmuel Sagiv (ISMM, 2000)

Checking Cleanness in Linked Lists. - Nurit Dor; Michael Rodeh; Shmuel Sagiv (SAS, 2000)

TVLA: A System for Implementing Static Analyses. - Tal Lev-Ami; Shmuel Sagiv (SAS, 2000)

Interprocedural Shape Analysis for Recursive Programs. - Noam Rinetzky; Shmuel Sagiv (CC, 2001)

Heap Profiling for Space-Efficient Java. - Ran Shaham; Elliot K. Kolodner; Shmuel Sagiv (PLDI, 2001)

Cleanness Checking of String Manipulations in C Programs via Integer Analysis. - Nurit Dor; Michael Rodeh; Shmuel Sagiv (SAS, 2001)

Kleene's Logic with Equality. - Flemming Nielson; Hanne Riis Nielson; Shmuel Sagiv (Inf. Process. Lett., 2001)

Shape Analysis and Applications. - Reinhard Wilhelm; Thomas W. Reps; Shmuel Sagiv (The Compiler Design Handbook, 2002)

Online Subpath Profiling. - David Oren; Yossi Matias; Shmuel Sagiv (CC, 2002)

Estimating the impact of heap liveness information on space consumption in Java. - Ran Shaham; Elliot K. Kolodner; Shmuel Sagiv (MSP/ISMM, 2002)

Semantic Minimization of 3-Valued Propositional Formulae. - Thomas W. Reps; Alexey Loginov; Shmuel Sagiv (LICS, 2002)

Deriving Specialized Program Analyses for Certifying Component-Client Conformance. - G. Ramalingam; Alex Varshavsky; John Field; Deepak Goyal; Shmuel Sagiv (PLDI, 2002)

Compactly Representing First-Order Structures for Static Analysis. - Roman Manevich; G. Ramalingam; John Field; Deepak Goyal; Shmuel Sagiv (SAS, 2002)

Parametric shape analysis via 3-valued logic. - Shmuel Sagiv; Thomas W. Reps; Reinhard Wilhelm (ACM Trans. Program. Lang. Syst., 2002)

CSSV: towards a realistic tool for statically detecting all buffer overflows in C. - Nurit Dor; Michael Rodeh; Shmuel Sagiv (PLDI, 2003)

Automatically Verifying Concurrent Queue Algorithms. - Eran Yahav; Shmuel Sagiv (SoftMC@CAV, 2003)

Verification via Structure Simulation. - Neil Immerman; Alexander Moshe Rabinovich; Thomas W. Reps; Shmuel Sagiv; Greta Yorsh (CAV, 2004)

Static Program Analysis via 3-Valued Logic. - Thomas W. Reps; Shmuel Sagiv; Reinhard Wilhelm (CAV, 2004)

The Boundary Between Decidability and Undecidability for Transitive-Closure Logics. - Neil Immerman; Alexander Moshe Rabinovich; Thomas W. Reps; Shmuel Sagiv; Greta Yorsh (CSL, 2004)

TVLA: A system for generating abstract interpreters. - Tal Lev-Ami; Roman Manevich; Shmuel Sagiv (IFIP Congress Topical Sessions, 2004)

Partially Disjunctive Heap Abstraction. - Roman Manevich; Shmuel Sagiv; Ganesan Ramalingam; John Field (SAS, 2004)

Numeric Domains with Summarized Dimensions. - Denis Gopan; Frank DiMaio; Nurit Dor; Thomas W. Reps; Shmuel Sagiv (TACAS, 2004)

Symbolically Computing Most-Precise Abstract Operations for Shape Analysis. - Greta Yorsh; Thomas W. Reps; Shmuel Sagiv (TACAS, 2004)

Symbolic Implementation of the Best Transformer. - Thomas W. Reps; Shmuel Sagiv; Greta Yorsh (VMCAI, 2004)

On the Expressive Power of Canonical Abstraction. - Shmuel Sagiv (VMCAI, 2004)

Abstraction Refinement via Inductive Learning. - Alexey Loginov; Thomas W. Reps; Shmuel Sagiv (CAV, 2005)

Optimizing C Multithreaded Memory Management Using Thread-Local Storage. - Yair Sade; Shmuel Sagiv; Ran Shaham (CC, 2005)

A framework for numeric analysis of array operations. - Denis Gopan; Thomas W. Reps; Shmuel Sagiv (POPL, 2005)

A semantics for procedure local heaps and its abstractions. - Noam Rinetzky; Jörg Bauer 001; Thomas W. Reps; Shmuel Sagiv; Reinhard Wilhelm (POPL, 2005)

Interprocedural Shape Analysis for Cutpoint-Free Programs. - Noam Rinetzky; Mooly Sagiv; Eran Yahav (SAS, 2005)

Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. - Roman Manevich; Eran Yahav; Ganesan Ramalingam; Shmuel Sagiv (VMCAI, 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; et al. (VSTTE, 2005)

Automatic Assume/Guarantee Reasoning for Heap-Manipulating Programs: Ongoing Work. - Greta Yorsh; Alexey Skidanov; Thomas W. Reps; Shmuel Sagiv (AIOOL@VMCAI, 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)

Refinement-Based Verification for Possibly-Cyclic Lists. - Alexey Loginov; Thomas W. Reps; Mooly Sagiv (Program Analysis and Compilation, 2006)

Abstract Counterexample-Based Refinement for Powerset Domains. - Roman Manevich; John Field; Thomas A. Henzinger; G. Ramalingam; Mooly Sagiv (Program Analysis and Compilation, 2006)

An Appreciation of the Work of Reinhard Wilhelm. - Thomas W. Reps; Mooly Sagiv; Jörg Bauer 001 (Program Analysis and Compilation, 2006)

Abstraction for Shape Analysis with Fast and Precise Transformers. - Tal Lev-Ami; Neil Immerman; Shmuel Sagiv (CAV, 2006)

Testing, abstraction, theorem proving: better together! - Greta Yorsh; Thomas Ball 001; Mooly Sagiv (ISSTA, 2006)

Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm. - Alexey Loginov; Thomas W. Reps; Mooly Sagiv (SAS, 2006)

Combining Shape Analyses by Intersecting Abstractions. - Gilad Arnold; Roman Manevich; Mooly Sagiv; Ran Shaham (VMCAI, 2006)

Verifying Temporal Heap Properties Specified via Evolution Logic. - Eran Yahav; Thomas W. Reps; Shmuel Sagiv; Reinhard Wilhelm (Log. J. IGPL, 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)

Shape Analysis and Applications. - Thomas W. Reps; Mooly Sagiv; Reinhard Wilhelm (The Compiler Design Handbook, 2nd ed., 2007)

Local Reasoning for Storable Locks and Threads. - Alexey Gotsman; Josh Berdine; Byron Cook; Noam Rinetzky; Mooly Sagiv (APLAS, 2007)

Labelled Clauses. - Tal Lev-Ami; Christoph Weidenbach; Thomas W. Reps; Mooly Sagiv (CADE, 2007)

Comparison Under Abstraction for Verifying Linearizability. - Daphna Amit; Noam Rinetzky; Thomas W. Reps; Mooly Sagiv; Eran Yahav (CAV, 2007)

Leaping Loops in the Presence of Abstraction. - Thomas Ball 001; Orna Kupferman; Mooly Sagiv (CAV, 2007)

Revamping TVLA: Making Parametric Shape Analysis Competitive. - Igor Bogudlov; Tal Lev-Ami; Thomas W. Reps; Mooly Sagiv (CAV, 2007)

Modular Shape Analysis for Dynamically Encapsulated Programs. - Noam Rinetzky; Arnd Poetzsch-Heffter; Ganesan Ramalingam; Mooly Sagiv; Eran Yahav (ESOP, 2007)

Thread-modular shape analysis. - Alexey Gotsman; Josh Berdine; Byron Cook; Mooly Sagiv (PLDI, 2007)

Cartesian Partial-Order Reduction. - Guy Gueta; Cormac Flanagan; Eran Yahav; Mooly Sagiv (SPIN, 2007)

Shape Analysis by Graph Decomposition. - Roman Manevich; Josh Berdine; Byron Cook; G. Ramalingam; Mooly Sagiv (TACAS, 2007)

Constructing Specialized Shape Analyses for Uniform Change. - Tal Lev-Ami; Mooly Sagiv; Neil Immerman; Thomas W. Reps (VMCAI, 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)

Scaling model checking of dataraces using dynamic information. - Ohad Shacham; Mooly Sagiv; Assaf Schuster (J. Parallel Distributed Comput., 2007)

Logical characterizations of heap abstractions. - Greta Yorsh; Thomas W. Reps; Mooly Sagiv; Reinhard Wilhelm (ACM Trans. Comput. Log., 2007)

Introduction to special ESOP'05 issue. - Mooly Sagiv (ACM Trans. Program. Lang. Syst., 2007)

Thread Quantification for Concurrent Shape Analysis. - Josh Berdine; Tal Lev-Ami; Roman Manevich; G. Ramalingam; Shmuel Sagiv (CAV, 2008)

Proving Conditional Termination. - Byron Cook; Sumit Gulwani; Tal Lev-Ami; Andrey Rybalchenko; Mooly Sagiv (CAV, 2008)

Ranking Abstractions. - Aziem Chawdhary; Byron Cook; Sumit Gulwani; Mooly Sagiv; Hongseok Yang (ESOP, 2008)

Customization change impact analysis for erp professionals via program slicing. - Nurit Dor; Tal Lev-Ami; Shay Litvak; Mooly Sagiv; Dror Weiss (ISSTA, 2008)

Heap Decomposition for Concurrent Shape Analysis. - Roman Manevich; Tal Lev-Ami; Mooly Sagiv; Ganesan Ramalingam; Josh Berdine (SAS, 2008)

On the complexity of partially-flow-sensitive alias analysis. - Noam Rinetzky; G. Ramalingam; Shmuel Sagiv; Eran Yahav (ACM Trans. Program. Lang. Syst., 2008)

Abstract Transformers for Thread Correlation Analysis. - Michal Segalov; Tal Lev-Ami; Roman Manevich; Ganesan Ramalingam; Mooly Sagiv (APLAS, 2009)

Generalizing DPLL to Richer Logics. - Kenneth L. McMillan; Andreas Kuehlmann; Mooly Sagiv (CAV, 2009)

09301 Abstracts Collection - Typing, Analysis, and Verification of Heap-Manipulating Programs. - Mooly Sagiv; Arnd Poetzsch-Heffter; Peter W. O'Hearn (Typing, Analysis and Verification of Heap-Manipulating Programs, 2009)

09301 Executive Summary - Typing, Analysis, and Verification of Heap-Manipulating Programs. - Mooly Sagiv; Arnd Poetzsch-Heffter; Peter W. O'Hearn (Typing, Analysis and Verification of Heap-Manipulating Programs, 2009)

A combination framework for tracking partition sizes. - Sumit Gulwani; Tal Lev-Ami; Mooly Sagiv (POPL, 2009)

Thread-Modular Shape Analysis. - Mooly Sagiv (VMCAI, 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 001; Greta Yorsh (Log. Methods Comput. Sci., 2009)

Self-stabilization preserving compiler. - Shlomi Dolev; Yinnon A. Haviv; Mooly Sagiv (ACM Trans. Program. Lang. Syst., 2009)

Data Structure Fusion. - Peter Hawkins; Alex Aiken; Kathleen Fisher; Martin C. Rinard; Mooly Sagiv (APLAS, 2010)

Specifying and verifying sparse matrix codes. - Gilad Arnold; Johannes Hölzl; Ali Sinan Köksal; Rastislav Bodík; Mooly Sagiv (ICFP, 2010)

A simple inductive synthesis methodology and its applications. - Shachar Itzhaky; Sumit Gulwani; Neil Immerman; Mooly Sagiv (OOPSLA, 2010)

A dynamic evaluation of the precision of static heap abstractions. - Percy Liang; Omer Tripp; Mayur Naik; Mooly Sagiv (OOPSLA, 2010)

Statically Inferring Complex Heap, Array, and Numeric Invariants. - Bill McCloskey; Thomas W. Reps; Mooly Sagiv (SAS, 2010)

Field-sensitive program dependence analysis. - Shay Litvak; Nurit Dor; Rastislav Bodík; Noam Rinetzky; Mooly Sagiv (SIGSOFT FSE, 2010)

Decidable fragments of many-sorted logic. - Aharon Abadi; Alexander Rabinovich; Mooly Sagiv (J. Symb. Comput., 2010)

A relational approach to interprocedural shape analysis. - Bertrand Jeannet; Alexey Loginov; Thomas W. Reps; 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)

Verifying safety properties of concurrent heap-manipulating programs. - Eran Yahav; Mooly Sagiv (ACM Trans. Program. Lang. Syst., 2010)

Automatic fine-grain locking using shape properties. - Guy Golan-Gueta; Nathan Grasso Bronson; Alex Aiken; G. Ramalingam; Mooly Sagiv; Eran Yahav (OOPSLA, 2011)

Testing atomicity of composed concurrent operations. - Ohad Shacham; Nathan Grasso Bronson; Alex Aiken; Mooly Sagiv; Martin T. Vechev; Eran Yahav (OOPSLA, 2011)

HAWKEYE: effective discovery of dataflow impediments to parallelization. - Omer Tripp; Greta Yorsh; John Field; Mooly Sagiv (OOPSLA, 2011)

Precise and compact modular procedure summaries for heap manipulating programs. - Isil Dillig; Thomas Dillig; Alex Aiken; Mooly Sagiv (PLDI, 2011)

Data representation synthesis. - Peter Hawkins; Alex Aiken; Kathleen Fisher; Martin C. Rinard; Mooly Sagiv (PLDI, 2011)

Eventually Consistent Transactions. - Sebastian Burckhardt; Daan Leijen; Manuel Fähndrich; Mooly Sagiv (ESOP, 2012)

Reasoning about Lock Placements. - Peter Hawkins; Alex Aiken; Kathleen Fisher; Martin C. Rinard; Mooly Sagiv (ESOP, 2012)

Understanding the behavior of database operations under program control. - Juan M. Tamayo; Alex Aiken; Nathan Grasso Bronson; Mooly Sagiv (OOPSLA, 2012)

Concurrent data representation synthesis. - Peter Hawkins; Alex Aiken; Kathleen Fisher; Martin C. Rinard; Mooly Sagiv (PLDI, 2012)

JANUS: exploiting parallelism via hindsight. - Omer Tripp; Roman Manevich; John Field; Mooly Sagiv (PLDI, 2012)

Abstractions from tests. - Mayur Naik; Hongseok Yang; Ghila Castelnuovo; Mooly Sagiv (POPL, 2012)

An introduction to data representation synthesis. - Peter Hawkins; Martin C. Rinard; Alex Aiken; Mooly Sagiv; Kathleen Fisher (Commun. ACM, 2012)

POPL'11 program chair's report. - Mooly Sagiv (ACM SIGPLAN Notices, 2012)

Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs. - Jörg Kreiker; Thomas W. Reps; Noam Rinetzky; Mooly Sagiv; Reinhard Wilhelm; Eran Yahav (Programming Logics, 2013)

Effectively-Propositional Reasoning about Reachability in Linked Data Structures. - Shachar Itzhaky; Anindya Banerjee 001; Neil Immerman; Aleksandar Nanevski; Mooly Sagiv (CAV, 2013)

Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning. - Shachar Itzhaky; Sumit Gulwani; Neil Immerman; Mooly Sagiv (LPAR, 2013)

Turning nondeterminism into parallelism. - Omer Tripp; Eric Koskinen; Mooly Sagiv (OOPSLA, 2013)

Concurrent libraries with foresight. - Guy Golan-Gueta; G. Ramalingam; Mooly Sagiv; Eran Yahav (PLDI, 2013)

Principles of POPL. - Derek Dreyer; John Field; Roberto Giacobazzi; Michael Hicks 001; Suresh Jagannathan; Mooly Sagiv; Peter Sewell; Philip Wadler (ACM SIGPLAN Notices, 2013)

Property-Directed Shape Analysis. - Shachar Itzhaky; Nikolaj S. Bjørner; Thomas W. Reps; Mooly Sagiv; Aditya V. Thakur (CAV, 2014)

Checking Linearizability of Encapsulated Extended Operations. - Oren Zomer; Guy Golan-Gueta; G. Ramalingam; Mooly Sagiv (ESOP, 2014)

Verifying atomicity via data independence. - Ohad Shacham; Eran Yahav; Guy Golan-Gueta; Alex Aiken; Nathan Grasso Bronson; Mooly Sagiv; Martin T. Vechev (ISSTA, 2014)

VeriCon: towards verifying controller programs in software-defined networks. - Thomas Ball 001; Nikolaj S. Bjørner; Aaron Gember; Shachar Itzhaky; Aleksandr Karbyshev; Mooly Sagiv; Michael Schapira; Asaf Valadarsky (PLDI, 2014)

Modular reasoning about heap paths via effectively propositional formulas. - Shachar Itzhaky; Anindya Banerjee 001; Neil Immerman; Ori Lahav 001; Aleksandar Nanevski; Mooly Sagiv (POPL, 2014)

Automatic semantic locking. - Guy Golan-Gueta; G. Ramalingam; Mooly Sagiv; Eran Yahav (PPoPP, 2014)

Verifying Isolation Properties in the Presence of Middleboxes. - Aurojit Panda; Ori Lahav 001; Katerina J. Argyraki; Mooly Sagiv; Scott Shenker (CoRR, 2014)

Composing concurrency control. - Ofri Ziv; Alex Aiken; Guy Golan-Gueta; G. Ramalingam; Mooly Sagiv (PLDI, 2015)

Decentralizing SDN Policies. - Oded Padon; Neil Immerman; Aleksandr Karbyshev; Ori Lahav 001; Mooly Sagiv; Sharon Shoham (POPL, 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 (SAS, 2015)

New Directions for Network Verification. - Aurojit Panda; Katerina J. Argyraki; Mooly Sagiv; Michael Schapira; Scott Shenker (SNAPL, 2015)

Simple Invariants for Proving the Safety of Distributed Protocols (Invited Talk). - Mooly Sagiv (FSTTCS, 2016)

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

Decidability of inferring inductive invariants. - Oded Padon; Neil Immerman; Sharon Shoham; Aleksandr Karbyshev; Mooly Sagiv (POPL, 2016)

Verifying Equivalence of Spark Programs. - Shelly Grossman; Sara Cohen; Shachar Itzhaky; Noam Rinetzky; Mooly Sagiv (CAV (2), 2017)

Abduction for Learning Smart City Rules. - Nikolaj S. Bjørner; Maria-Cristina V. Marinescu; Mooly Sagiv (GCAI, 2017)

Verification in the Age of Microservices. - Aurojit Panda; Mooly Sagiv; Scott Shenker (HotOS, 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 (ICDT, 2017)

Verifying Reachability in Networks with Mutable Datapaths. - Aurojit Panda; Ori Lahav 001; Katerina J. Argyraki; Mooly Sagiv; Scott Shenker (NSDI, 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 (VMCAI, 2017)

Conjunctive Abstract Interpretation Using Paramodulation. - Or Ozeri; Oded Padon; Noam Rinetzky; Mooly Sagiv (VMCAI, 2017)

Modular Safety Verification for Stateful Networks. - Kalev Alpernas; Roman Manevich; Aurojit Panda; Mooly Sagiv; Scott Shenker; Sharon Shoham; Yaron Velner (CoRR, 2017)

Paxos made EPR: decidable reasoning about distributed protocols. - Oded Padon; Giuliano Losa; Mooly Sagiv; Sharon Shoham (Proc. ACM Program. Lang., 2017)

Synthesis of circular compositional program proofs via abduction. - Isil Dillig; Thomas Dillig; Boyang Li 002; Kenneth L. McMillan; Mooly Sagiv (Int. J. Softw. Tools Technol. Transf., 2017)

Automatic Scalable Atomicity via Semantic Locking. - Guy Golan-Gueta; G. Ramalingam; Mooly Sagiv; Eran Yahav (ACM Trans. Parallel Comput., 2017)

Verifying Properties of Binarized Deep Neural Networks. - Nina Narodytska; Shiva Prasad Kasiviswanathan; Leonid Ryzhyk; Mooly Sagiv; Toby Walsh (AAAI, 2018)

Core-Guided Minimal Correction Set and Core Enumeration. - Nina Narodytska; Nikolaj S. Bjørner; Maria-Cristina V. Marinescu; Mooly Sagiv (IJCAI, 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 (PLDI, 2018)

Abstract Interpretation of Stateful Networks. - Kalev Alpernas; Roman Manevich; Aurojit Panda; Mooly Sagiv; Scott Shenker; Sharon Shoham; Yaron Velner (SAS, 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 (SAT, 2018)

Secure serverless computing using dynamic information flow control. - Kalev Alpernas; Cormac Flanagan; Sadjad Fouladi; Leonid Ryzhyk; Mooly Sagiv; Thomas Schmitz 001; Keith Winstein (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)

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)

Inferring Inductive Invariants from Phase Structures. - Yotam M. Y. Feldman; James R. Wilcox; Sharon Shoham; Mooly Sagiv (CAV (2), 2019)

Synthesizing Cluster Management Code for Distributed Systems. - Lalith Suresh 001; João Loff; Nina Narodytska; Leonid Ryzhyk; Mooly Sagiv; Brian Oki (HotOS, 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 (PLDI, 2019)

Automating Cluster Management with Weave. - Lalith Suresh 001; João Loff; Faria Kalim; Nina Narodytska; Leonid Ryzhyk; Sahan Gamage; Brian Oki; Zeeshan Lokhandwala; Mukesh Hira; Mooly Sagiv (CoRR, 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)

Bounded Quantifier Instantiation for Checking Inductive Invariants. - Yotam M. Y. Feldman; Oded Padon; Neil Immerman; Mooly Sagiv; Sharon Shoham (Log. Methods Comput. Sci., 2019)

Invited Talk: Harnessing SMT Solvers for Verifying Low Level Programs. - Mooly Sagiv (SMT, 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)

Complexity and information in invariant inference. - Yotam M. Y. Feldman; Neil Immerman; Mooly Sagiv; Sharon Shoham (Proc. ACM Program. Lang., 2020)

Summing up Smart Transitions. - Neta Elad; Sophie Rain; Neil Immerman; Laura Kovács; Mooly Sagiv (CAV (1), 2021)

Cloud-Scale Runtime Verification of Serverless Applications. - Kalev Alpernas; Aurojit Panda; Leonid Ryzhyk; Mooly Sagiv (SoCC, 2021)

Phoenix: A Formally Verified Regenerating Vault. - Uri Kirstein; Shelly Grossman; Michael Mirkin; James Wilcox 004; Ittay Eyal; Mooly Sagiv (CoRR, 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)

Learning the boundary of inductive invariants. - Yotam M. Y. Feldman; Mooly Sagiv; Sharon Shoham; James R. Wilcox (Proc. ACM Program. Lang., 2021)

Blockaid: Data Access Policy Enforcement for Web Applications. - Wen Zhang; Eric Sheng; Michael Alan Chang; Aurojit Panda; Mooly Sagiv; Scott Shenker (OSDI, 2022)

This is not the End: Rethinking Serverless Function Termination. - Kalev Alpernas; Aurojit Panda; Mooly Sagiv (CoRR, 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)

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)

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., 2023)

Harnessing SMT Solvers for Reasoning about DeFi Protocols. - Mooly Sagiv (FMCAD, 2024)

A Decidable Case of Query Determinacy: Project-Select Views. - Wen Zhang; Aurojit Panda; Mooly Sagiv; Scott Shenker (CoRR, 2024)

Practical Verification of Smart Contracts using Memory Splitting. - Shelly Grossman; John Toman; Alexander Bakst; Sameer Arora; Mooly Sagiv; Chandrakana Nandi (Proc. ACM Program. Lang., 2024)