Mooly Sagiv - RankMe

150 papers A* 27A 24B 22C 1Misc 1Journal 53Unranked 19

Year	Rank	Type	Title / Venue / Authors
2024	J	`jnl`	A Decidable Case of Query Determinacy: Project-Select Views. CoRR Wen Zhang, Aurojit Panda, Mooly Sagiv, Scott Shenker
2024	B	`conf`	Harnessing SMT Solvers for Reasoning about DeFi Protocols. FMCAD Mooly Sagiv
2024	J	`jnl`	Practical Verification of Smart Contracts using Memory Splitting. Proc. ACM Program. Lang. Shelly Grossman, John Toman, Alexander Bakst, Sameer Arora, Mooly Sagiv, Chandrakana Nandi
2023	J	`jnl`	Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols. Proc. ACM Program. Lang. Orr Tamir, Marcelo Taube, Kenneth L. McMillan, Sharon Shoham, Jon Howell, Guy Gueta, Mooly Sagiv
2023	J	`jnl`	Relaxed Effective Callback Freedom: A Parametric Correctness Condition for Sequential Modules With Callbacks. IEEE Trans. Dependable Secur. Comput. Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodríguez-Núñez, Albert Rubio, Mooly Sagiv
2022	A*	`conf`	Blockaid: Data Access Policy Enforcement for Web Applications. OSDI Wen Zhang, Eric Sheng, Michael Alan Chang, Aurojit Panda, Mooly Sagiv, Scott Shenker
2022	J	`jnl`	Blockaid: Data Access Policy Enforcement for Web Applications. CoRR Wen Zhang, Eric Sheng, Michael Alan Chang, Aurojit Panda, Mooly Sagiv, Scott Shenker
2022	J	`jnl`	Property-directed reachability as abstract interpretation in the monotone theory. Proc. ACM Program. Lang. Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox
2022	J	`jnl`	This is not the End: Rethinking Serverless Function Termination. CoRR Kalev Alpernas, Aurojit Panda, Mooly Sagiv
2021	—	`conf`	Cloud-Scale Runtime Verification of Serverless Applications. SoCC Kalev Alpernas, Aurojit Panda, Leonid Ryzhyk, Mooly Sagiv
2021	J	`jnl`	Learning the boundary of inductive invariants. Proc. ACM Program. Lang. Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox
2021	J	`jnl`	Phoenix: A Formally Verified Regenerating Vault. CoRR Uri Kirstein, Shelly Grossman, Michael Mirkin, James Wilcox, Ittay Eyal, Mooly Sagiv
2021	J	`jnl`	Property-Directed Reachability as Abstract Interpretation in the Monotone Theory. CoRR Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox
2021	J	`jnl`	Some Complexity Results for Stateful Network Verification. CoRR Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner
2021	J	`jnl`	Summing Up Smart Transitions. CoRR Neta Elad, Sophie Rain, Neil Immerman, Laura Kovács, Mooly Sagiv
2021	—	`conf`	Summing up Smart Transitions. CAV (1) Neta Elad, Sophie Rain, Neil Immerman, Laura Kovács, Mooly Sagiv
2021	J	`jnl`	Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. CoRR Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
2021	J	`jnl`	Temporal prophecy for proving temporal properties of infinite-state systems. Formal Methods Syst. Des. Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
2020	J	`jnl`	Complexity and information in invariant inference. Proc. ACM Program. Lang. Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, Sharon Shoham
2020	—	`conf`	Invited Talk: Harnessing SMT Solvers for Verifying Low Level Programs. SMT Mooly Sagiv
2020	J	`jnl`	Learning the Boundary of Inductive Invariants. CoRR Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox
2020	J	`jnl`	Taming callbacks for smart contract modularity. Proc. ACM Program. Lang. Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodríguez-Núñez, Albert Rubio, Mooly Sagiv
2019	J	`jnl`	Automating Cluster Management with Weave. CoRR Lalith Suresh, João Loff, Faria Kalim, Nina Narodytska, Leonid Ryzhyk, Sahan Gamage, Brian Oki, Zeeshan Lokhandwala, Mukesh Hira, Mooly Sagiv
2019	J	`jnl`	Bounded Quantifier Instantiation for Checking Inductive Invariants. Log. Methods Comput. Sci. Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham
2019	J	`jnl`	Complexity and Information in Invariant Inference. CoRR Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, Sharon Shoham
2019	—	`conf`	Inferring Inductive Invariants from Phase Structures. CAV (2) Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv
2019	J	`jnl`	Inferring Inductive Invariants from Phase Structures. CoRR Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv
2019	A*	`conf`	Simple and precise static analysis of untrusted Linux kernel extensions. PLDI Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk, Mooly Sagiv
2019	J	`jnl`	Some complexity results for stateful network verification. Formal Methods Syst. Des. Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner
2019	A	`conf`	Synthesizing Cluster Management Code for Distributed Systems. HotOS Lalith Suresh, João Loff, Nina Narodytska, Leonid Ryzhyk, Mooly Sagiv, Brian Oki
2018	B	`conf`	Abstract Interpretation of Stateful Networks. SAS Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner
2018	A	`conf`	Constrained Image Generation Using Binarized Neural Networks with Decision Procedures. SAT Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj S. Bjørner, Mooly Sagiv
2018	J	`jnl`	Constrained Image Generation Using Binarized Neural Networks with Decision Procedures. CoRR Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj S. Bjørner, Mooly Sagiv
2018	A*	`conf`	Core-Guided Minimal Correction Set and Core Enumeration. IJCAI Nina Narodytska, Nikolaj S. Bjørner, Maria-Cristina V. Marinescu, Mooly Sagiv
2018	A*	`conf`	Modularity for decidability of deductive verification with applications to distributed systems. PLDI Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, Doug Woos
2018	J	`jnl`	Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts. CoRR Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, Yoni Zohar
2018	J	`jnl`	Online detection of effectively callback free objects with applications to smart contracts. Proc. ACM Program. Lang. Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, Yoni Zohar
2018	J	`jnl`	Reducing liveness to safety in first-order logic. Proc. ACM Program. Lang. Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham
2018	J	`jnl`	Secure Serverless Computing Using Dynamic Information Flow Control. CoRR Kalev Alpernas, Cormac Flanagan, Sadjad Fouladi, Leonid Ryzhyk, Mooly Sagiv, Thomas Schmitz, Keith Winstein
2018	J	`jnl`	Secure serverless computing using dynamic information flow control. Proc. ACM Program. Lang. Kalev Alpernas, Cormac Flanagan, Sadjad Fouladi, Leonid Ryzhyk, Mooly Sagiv, Thomas Schmitz, Keith Winstein
2018	B	`conf`	Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. FMCAD Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
2018	A*	`conf`	Verifying Properties of Binarized Deep Neural Networks. AAAI Nina Narodytska, Shiva Prasad Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, Toby Walsh
2017	—	`conf`	Abduction for Learning Smart City Rules. GCAI Nikolaj S. Bjørner, Maria-Cristina V. Marinescu, Mooly Sagiv
2017	J	`jnl`	Automatic Scalable Atomicity via Semantic Locking. ACM Trans. Parallel Comput. Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv, Eran Yahav
2017	—	`conf`	Bounded Quantifier Instantiation for Checking Inductive Invariants. TACAS (1) Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham
2017	J	`jnl`	Bounded Quantifier Instantiation for Checking Inductive Invariants. CoRR Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham
2017	B	`conf`	Conjunctive Abstract Interpretation Using Paramodulation. VMCAI Or Ozeri, Oded Padon, Noam Rinetzky, Mooly Sagiv
2017	J	`jnl`	Modular Safety Verification for Stateful Networks. CoRR Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner
2017	A	`conf`	On the Automated Verification of Web Applications with Embedded SQL. ICDT Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, Florian Zuleger
2017	J	`jnl`	Paxos Made EPR: Decidable Reasoning about Distributed Protocols. CoRR Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham
2017	J	`jnl`	Paxos made EPR: decidable reasoning about distributed protocols. Proc. ACM Program. Lang. Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham
2017	B	`conf`	Property Directed Reachability for Proving Absence of Concurrent Modification Errors. VMCAI Asya Frumkin, Yotam M. Y. Feldman, Ondrej Lhoták, Oded Padon, Mooly Sagiv, Sharon Shoham
2017	J	`jnl`	Synthesis of circular compositional program proofs via abduction. Int. J. Softw. Tools Technol. Transf. Isil Dillig, Thomas Dillig, Boyang Li, Kenneth L. McMillan, Mooly Sagiv
2017	A	`conf`	Verification in the Age of Microservices. HotOS Aurojit Panda, Mooly Sagiv, Scott Shenker
2017	—	`conf`	Verifying Equivalence of Spark Programs. CAV (2) Shelly Grossman, Sara Cohen, Shachar Itzhaky, Noam Rinetzky, Mooly Sagiv
2017	J	`jnl`	Verifying Properties of Binarized Deep Neural Networks. CoRR Nina Narodytska, Shiva Prasad Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, Toby Walsh
2017	Misc	`conf`	Verifying Reachability in Networks with Mutable Datapaths. NSDI Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker
2016	A*	`conf`	Decidability of inferring inductive invariants. POPL Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv
2016	A*	`conf`	Ivy: safety verification by interactive generalization. PLDI Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham
2016	J	`jnl`	On the automated verification of web applications with embedded SQL. CoRR Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, Florian Zuleger
2016	—	`conf`	Simple Invariants for Proving the Safety of Distributed Protocols (Invited Talk). FSTTCS Mooly Sagiv
2016	A	`conf`	Some Complexity Results for Stateful Network Verification. TACAS Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham
2016	J	`jnl`	Verifying Reachability in Networks with Mutable Datapaths. CoRR Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker
2015	B	`conf`	Automatic scalable atomicity via semantic locking. PPoPP Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv, Eran Yahav
2015	A*	`conf`	Composing concurrency control. PLDI Ofri Ziv, Alex Aiken, Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv
2015	A*	`conf`	Decentralizing SDN Policies. POPL Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham
2015	B	`conf`	Modularity in Lattices: A Case Study on the Correspondence Between Top-Down and Bottom-Up Analysis. SAS Ghila Castelnuovo, Mayur Naik, Noam Rinetzky, Mooly Sagiv, Hongseok Yang
2015	—	`conf`	New Directions for Network Verification. SNAPL Aurojit Panda, Katerina J. Argyraki, Mooly Sagiv, Michael Schapira, Scott Shenker
2014	B	`conf`	Automatic semantic locking. PPoPP Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv, Eran Yahav
2014	A	`conf`	Checking Linearizability of Encapsulated Extended Operations. ESOP Oren Zomer, Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv
2014	A*	`conf`	Modular reasoning about heap paths via effectively propositional formulas. POPL Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv
2014	A*	`conf`	Property-Directed Shape Analysis. CAV Shachar Itzhaky, Nikolaj S. Bjørner, Thomas W. Reps, Mooly Sagiv, Aditya V. Thakur
2014	A*	`conf`	VeriCon: towards verifying controller programs in software-defined networks. PLDI Thomas Ball, Nikolaj S. Bjørner, Aaron Gember, Shachar Itzhaky, Aleksandr Karbyshev, Mooly Sagiv, Michael Schapira, Asaf Valadarsky
2014	J	`jnl`	Verifying Isolation Properties in the Presence of Middleboxes. CoRR Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker
2014	A	`conf`	Verifying atomicity via data independence. ISSTA Ohad Shacham, Eran Yahav, Guy Golan-Gueta, Alex Aiken, Nathan Grasso Bronson, Mooly Sagiv, Martin T. Vechev
2013	A*	`conf`	Concurrent libraries with foresight. PLDI Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv, Eran Yahav
2013	A*	`conf`	Effectively-Propositional Reasoning about Reachability in Linked Data Structures. CAV Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv
2013	—	`conf`	Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs. Programming Logics Jörg Kreiker, Thomas W. Reps, Noam Rinetzky, Mooly Sagiv, Reinhard Wilhelm, Eran Yahav
2013	J	`jnl`	Principles of POPL. ACM SIGPLAN Notices Derek Dreyer, John Field, Roberto Giacobazzi, Michael Hicks, Suresh Jagannathan, Mooly Sagiv, Peter Sewell, Philip Wadler
2013	B	`conf`	Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning. LPAR Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv
2013	A	`conf`	Synthesis of Circular Compositional Program Proofs via Abduction. TACAS Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Mooly Sagiv
2013	A	`conf`	Turning nondeterminism into parallelism. OOPSLA Omer Tripp, Eric Koskinen, Mooly Sagiv
2012	A*	`conf`	Abstractions from tests. POPL Mayur Naik, Hongseok Yang, Ghila Castelnuovo, Mooly Sagiv
2012	J	`jnl`	An introduction to data representation synthesis. Commun. ACM Peter Hawkins, Martin C. Rinard, Alex Aiken, Mooly Sagiv, Kathleen Fisher
2012	A*	`conf`	Concurrent data representation synthesis. PLDI Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv
2012	A	`conf`	Eventually Consistent Transactions. ESOP Sebastian Burckhardt, Daan Leijen, Manuel Fähndrich, Mooly Sagiv
2012	A*	`conf`	JANUS: exploiting parallelism via hindsight. PLDI Omer Tripp, Roman Manevich, John Field, Mooly Sagiv
2012	J	`jnl`	POPL'11 program chair's report. ACM SIGPLAN Notices Mooly Sagiv
2012	A	`conf`	Reasoning about Lock Placements. ESOP Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv
2012	A	`conf`	Understanding the behavior of database operations under program control. OOPSLA Juan M. Tamayo, Alex Aiken, Nathan Grasso Bronson, Mooly Sagiv
2011	A	`conf`	Automatic fine-grain locking using shape properties. OOPSLA Guy Golan-Gueta, Nathan Grasso Bronson, Alex Aiken, G. Ramalingam, Mooly Sagiv, Eran Yahav
2011	A*	`conf`	Data representation synthesis. PLDI Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv
2011	A	`conf`	HAWKEYE: effective discovery of dataflow impediments to parallelization. OOPSLA Omer Tripp, Greta Yorsh, John Field, Mooly Sagiv
2011	A*	`conf`	Precise and compact modular procedure summaries for heap manipulating programs. PLDI Isil Dillig, Thomas Dillig, Alex Aiken, Mooly Sagiv
2011	A*	`ed.`	Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011 POPL Thomas Ball, Mooly Sagiv
2011	A	`conf`	Testing atomicity of composed concurrent operations. OOPSLA Ohad Shacham, Nathan Grasso Bronson, Alex Aiken, Mooly Sagiv, Martin T. Vechev, Eran Yahav
2010	A	`conf`	A dynamic evaluation of the precision of static heap abstractions. OOPSLA Percy Liang, Omer Tripp, Mayur Naik, Mooly Sagiv
2010	J	`jnl`	A relational approach to interprocedural shape analysis. ACM Trans. Program. Lang. Syst. Bertrand Jeannet, Alexey Loginov, Thomas W. Reps, Mooly Sagiv
2010	A	`conf`	A simple inductive synthesis methodology and its applications. OOPSLA Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv
2010	B	`conf`	Data Structure Fusion. APLAS Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv
2010	J	`jnl`	Decidable fragments of many-sorted logic. J. Symb. Comput. Aharon Abadi, Alexander Rabinovich, Mooly Sagiv
2010	—	`conf`	Field-sensitive program dependence analysis. SIGSOFT FSE Shay Litvak, Nurit Dor, Rastislav Bodík, Noam Rinetzky, Mooly Sagiv
2010	J	`jnl`	Finite differencing of logical formulas for static analysis. ACM Trans. Program. Lang. Syst. Thomas W. Reps, Mooly Sagiv, Alexey Loginov
2010	A	`conf`	Specifying and verifying sparse matrix codes. ICFP Gilad Arnold, Johannes Hölzl, Ali Sinan Köksal, Rastislav Bodík, Mooly Sagiv
2010	B	`conf`	Statically Inferring Complex Heap, Array, and Numeric Invariants. SAS Bill McCloskey, Thomas W. Reps, Mooly Sagiv
2010	J	`jnl`	Verifying safety properties of concurrent heap-manipulating programs. ACM Trans. Program. Lang. Syst. Eran Yahav, Mooly Sagiv
2009	—	`conf`	09301 Abstracts Collection - Typing, Analysis, and Verification of Heap-Manipulating Programs. Typing, Analysis and Verification of Heap-Manipulating Programs Mooly Sagiv, Arnd Poetzsch-Heffter, Peter W. O'Hearn
2009	—	`conf`	09301 Executive Summary - Typing, Analysis, and Verification of Heap-Manipulating Programs. Typing, Analysis and Verification of Heap-Manipulating Programs Mooly Sagiv, Arnd Poetzsch-Heffter, Peter W. O'Hearn
2009	A*	`conf`	A combination framework for tracking partition sizes. POPL Sumit Gulwani, Tal Lev-Ami, Mooly Sagiv
2009	B	`conf`	Abstract Transformers for Thread Correlation Analysis. APLAS Michal Segalov, Tal Lev-Ami, Roman Manevich, Ganesan Ramalingam, Mooly Sagiv
2009	A*	`conf`	Generalizing DPLL to Richer Logics. CAV Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv
2009	J	`jnl`	Self-stabilization preserving compiler. ACM Trans. Program. Lang. Syst. Shlomi Dolev, Yinnon A. Haviv, Mooly Sagiv
2009	J	`jnl`	Simulating reachability using first-order logic with applications to verification of linked data structures Log. Methods Comput. Sci. Tal Lev-Ami, Neil Immerman, Thomas W. Reps, Mooly Sagiv, Siddharth Srivastava, Greta Yorsh
2009	B	`conf`	Thread-Modular Shape Analysis. VMCAI Mooly Sagiv
2009	—	`ed.`	Typing, Analysis and Verification of Heap-Manipulating Programs, 19.07. - 24.07.2009 Typing, Analysis and Verification of Heap-Manipulating Programs Peter W. O'Hearn, Arnd Poetzsch-Heffter, Mooly Sagiv
2008	A	`conf`	Customization change impact analysis for erp professionals via program slicing. ISSTA Nurit Dor, Tal Lev-Ami, Shay Litvak, Mooly Sagiv, Dror Weiss
2008	B	`conf`	Heap Decomposition for Concurrent Shape Analysis. SAS Roman Manevich, Tal Lev-Ami, Mooly Sagiv, Ganesan Ramalingam, Josh Berdine
2008	A*	`conf`	Proving Conditional Termination. CAV Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv
2008	A	`conf`	Ranking Abstractions. ESOP Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, Hongseok Yang
2007	J	`jnl`	A Logic of Reachable Patterns in Linked Data-Structures CoRR Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani
2007	J	`jnl`	A logic of reachable patterns in linked data-structures. J. Log. Algebraic Methods Program. Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani
2007	—	`conf`	Cartesian Partial-Order Reduction. SPIN Guy Gueta, Cormac Flanagan, Eran Yahav, Mooly Sagiv
2007	A*	`conf`	Comparison Under Abstraction for Verifying Linearizability. CAV Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, Eran Yahav
2007	B	`conf`	Constructing Specialized Shape Analyses for Uniform Change. VMCAI Tal Lev-Ami, Mooly Sagiv, Neil Immerman, Thomas W. Reps
2007	B	`conf`	Decidable Fragments of Many-Sorted Logic. LPAR Aharon Abadi, Alexander Moshe Rabinovich, Mooly Sagiv
2007	J	`jnl`	Introduction to special ESOP'05 issue. ACM Trans. Program. Lang. Syst. Mooly Sagiv
2007	A	`conf`	Labelled Clauses. CADE Tal Lev-Ami, Christoph Weidenbach, Thomas W. Reps, Mooly Sagiv
2007	A*	`conf`	Leaping Loops in the Presence of Abstraction. CAV Thomas Ball, Orna Kupferman, Mooly Sagiv
2007	B	`conf`	Local Reasoning for Storable Locks and Threads. APLAS Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv
2007	J	`jnl`	Logical characterizations of heap abstractions. ACM Trans. Comput. Log. Greta Yorsh, Thomas W. Reps, Mooly Sagiv, Reinhard Wilhelm
2007	A	`conf`	Modular Shape Analysis for Dynamically Encapsulated Programs. ESOP Noam Rinetzky, Arnd Poetzsch-Heffter, Ganesan Ramalingam, Mooly Sagiv, Eran Yahav
2007	C	`ed.`	Proceedings of the 6th International Symposium on Memory Management, ISMM 2007, Montreal, Quebec, Canada, October 21-22, 2007 ISMM Greg Morrisett, Mooly Sagiv
2007	—	`ed.`	Program Analysis and Compilation, Theory and Practice, Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday Program Analysis and Compilation Thomas W. Reps, Mooly Sagiv, Jörg Bauer
2007	A*	`conf`	Revamping TVLA: Making Parametric Shape Analysis Competitive. CAV Igor Bogudlov, Tal Lev-Ami, Thomas W. Reps, Mooly Sagiv
2007	J	`jnl`	Scaling model checking of dataraces using dynamic information. J. Parallel Distributed Comput. Ohad Shacham, Mooly Sagiv, Assaf Schuster
2007	—	`ch.`	Shape Analysis and Applications. The Compiler Design Handbook, 2nd ed. Thomas W. Reps, Mooly Sagiv, Reinhard Wilhelm
2007	A	`conf`	Shape Analysis by Graph Decomposition. TACAS Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv
2007	A*	`conf`	Thread-modular shape analysis. PLDI Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv
2006	B	`conf`	A Logic of Reachable Patterns in Linked Data-Structures. FoSSaCS Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani
2006	—	`conf`	Abstract Counterexample-Based Refinement for Powerset Domains. Program Analysis and Compilation Roman Manevich, John Field, Thomas A. Henzinger, G. Ramalingam, Mooly Sagiv
2006	—	`conf`	An Appreciation of the Work of Reinhard Wilhelm. Program Analysis and Compilation Thomas W. Reps, Mooly Sagiv, Jörg Bauer
2006	B	`conf`	Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm. SAS Alexey Loginov, Thomas W. Reps, Mooly Sagiv
2006	B	`conf`	Combining Shape Analyses by Intersecting Abstractions. VMCAI Gilad Arnold, Roman Manevich, Mooly Sagiv, Ran Shaham
2006	—	`conf`	Refinement-Based Verification for Possibly-Cyclic Lists. Program Analysis and Compilation Alexey Loginov, Thomas W. Reps, Mooly Sagiv
2006	A	`conf`	Testing, abstraction, theorem proving: better together! ISSTA Greta Yorsh, Thomas Ball, Mooly Sagiv
2005	—	`conf`	Automatic Verification of Strongly Dynamic Software Systems. VSTTE 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
2005	J	`jnl`	Establishing local temporal heap safety properties with applications to compile-time memory management. Sci. Comput. Program. Ran Shaham, Eran Yahav, Elliot K. Kolodner, Mooly Sagiv
2005	B	`conf`	Interprocedural Shape Analysis for Cutpoint-Free Programs. SAS Noam Rinetzky, Mooly Sagiv, Eran Yahav
2005	B	`conf`	Scaling model checking of dataraces using dynamic information. PPoPP Ohad Shacham, Mooly Sagiv, Assaf Schuster
2005	—	`conf`	Self-stabilization Preserving Compiler. Self-Stabilizing Systems Shlomi Dolev, Yinnon A. Haviv, Mooly Sagiv