Courses (2012-2013)

• 0368.3133 (Oct'12): Compilation Course.
• 0368.405101 (Oct'12): Program Analysis.

Research

My research focuses broadly on easing the task of developing reliable programs via program analysis. Current projects include:

• Shape Analysis. Inferring Properties of programs manipulating dynamically allocated data structures and pointers.
• Effective Programming with Relations. Compiling Programs with Relations into low level programs manipulating dynamically allocated data structures and pointers.
• Composing Concurrent Libraries. Easing the task of writing correct and efficient concurrent software using sophisticated libraries.

More information on current and past research here.

Some Talks

• Concurrent Data Representation SynthesisMicrosoft Research Cambridge August 2012 2011. [.pptx], [.pdf] Recorded Talk
• COLT: Testing and Verifying Atomicity of Composed Operations IMDEA Software March 2012 [.pptx], [.pdf
• TVLA: A system for inferring Quantified InvariantsSoftware Seminar at Stanford University 2008 [.pptx], [.pdf

Recent Papers

• An Introduction to Data Representation Synthesis. P. Hawkins, A. Aiken, K. Fisher, M. Rinard, and M. Sagiv. Communications of the ACM, research highlight, to appear.
• Transactional Objects with Foresight. Guy Golan Gueta, G. Ramalingam, Mooly Sagiv, and Eran Yahav. Submitted for publication
• Modular Lattices for Compositional Interprocedural Analysis. Ghila Castelnuovo, Mayur Naik, Noam Rinetzky, Mooly Sagiv, and Hongseok Yang. Submitted for publication
• Combining Program Analyses via Abduction. Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, and Mooly Sagiv. Submitted for publication
• Understanding the Behavior of Database Operations under Program Control. J. Tamayo, A. Aiken, N. Bronson and M. Sagiv. Proceedings of the International Conference on Object-Oriented Programming, Systems, Languages, and Applications, to appear, October 2012.
• Concurrent Data Representation Synthesis. P. Hawkins, A. Aiken, K. Fisher, M. Rinard, and M. Sagiv. Proceedings of the Conference on Programming Language Design and Implementation, pages 417-428, June 2012. (Best Paper Award)
• Reasoning About Lock Placements. P. Hawkins, A. Aiken, K. Fisher, M. Rinard, and M. Sagiv. Proceedings of the European Symposium on Programming, pages 336-356, March 2012.
• Janus: Exploiting Parallelism via Hindsight. Omer Tripp, Roman Manevich, John Field, and Mooly Sagiv. PLDI'12: ACM Conference on Programming Language Design and Implementation
• Abstractions from Tests. Mayur Naik, Hongseok Yang, Ghila Castelnuovo, and Mooly Sagiv. POPL'12.
• Testing Atomicity of Composed Concurrent Operations. O. Shacham, N. Bronson, A. Aiken, M. Sagiv, M. Vechev, and E. Yahav. Proceedings of the International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 51-64, October 2011.
• Automatic Fine-Grain Locking Using Shape Properties. G. Golan-Gueta, N. Bronson, A. Aiken, G. Ramalingam, M. Sagiv, E. Yahav. Proceedings of the International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 225-242, October 2011
• Data Representation Synthesis. P. Hawkins, A. Aiken, K. Fisher, and M. Sagiv. Proceedings of the Conference on Programming Language Design and Implementation, pages 38-49, June 2011. (Best Paper Award)
• Precise and Compact Modular Procedure Summaries for Heap Manipulating Programs. I. Dillig, T. Dillig, A. Aiken, and M. Sagiv. Proceedings of the Conference on Programming Language Design and Implementation. pages 567-577, June 2011.
• Hawkeye: Effective Discovery of Dataflow Impediments to Parallelization Omer Tripp, Greta Yorsh, John Field, and Mooly Sagiv OOPSLA'11: ACM Conference on Systems, Programming, Languages and Applications
• Data Structure Fusion. P. Hawkins, A. Aiken, K. Fisher, M.Rinard, and M. Sagiv. Proceedings of the Asian Symposium on Programming Languages and Systems, pages 204-221, November 2010.
• A Dynamic Evaluation of the Precision of Static Heap Abstractions Percy Liang, Omer Tripp, Mayur Naik, and Mooly Sagiv OOPSLA'10: ACM Conference on Systems, Programming, Languages and Applications
• Specifying and verifying sparse matrix codes. Gilad Arnold, Johannes Ho"lzl, Ali Sinan Ko"ksal, Rastislav Bodik, and Mooly Sagiv. ICFP 2010: 249-260
• A simple inductive synthesis methodology and its applications . Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv OOPSLA 2010: 36-46
• Statically Inferring Complex Heap, Array, and Numeric Invariants. Bill McCloskey, Thomas W. Reps, Mooly Sagiv. SAS 2010: 71-99
• Field-sensitive program dependence analysis. Shay Litvak, Nurit Dor, Rastislav Bodi'k, Noam Rinetzky, Mooly Sagiv: SIGSOFT FSE 2010: 287-296
• A relational approach to interprocedural shape analysis Bertrand Jeannet, Alexey Loginov, Thomas W. Reps, Mooly Sagiv. ACM Trans. Program. Lang. Syst. 32(2): (2010)
• Eran Yahav, Mooly Sagiv Verifying safety properties of concurrent heap-manipulating programs. ACM Trans. Program. Lang. Syst. 32(5): (2010)
• Finite differencing of logical formulas for static analysis. Thomas W. Reps, Mooly Sagiv, Alexey Loginov: ACM Trans. Program. Lang. Syst. 32(6): (2010)
• Decidable fragments of many-sorted logic.Aharon Abadi, Alexander Rabinovich, Mooly Sagiv: J. Symb. Comput. 45(2): 153-172 (2010)

Selected Publications

• An Introduction to Data Representation Synthesis.
• Testing Atomicity of Composed Concurrent Operations. O. Shacham, N. Bronson, A. Aiken, M. Sagiv, M. Vechev, and E. Yahav. Proceedings of the International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 51-64, October 2011.
• Eran Yahav, Mooly Sagiv Verifying safety properties of concurrent heap-manipulating programs. ACM Trans. Program. Lang. Syst. 32(5): (2010)
• Finite differencing of logical formulas for static analysis. Thomas W. Reps, Mooly Sagiv, Alexey Loginov: ACM Trans. Program. Lang. Syst. 32(6): (2010)
• 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. Logical Methods in Computer Science 5(2): (2009)
• Heap Decomposition for Concurrent Shape Analysis Roman Manevich, Tal Lev-Ami, Mooly Sagiv, Ganesan Ramalingam, Josh Berdine: SAS 2008: 363-377
• A semantics for procedure local heaps and its abstractions, N. Rinetzky, J. Bauer, T. Reps, M. Sagiv, and R. Wilhelm. POPL '05: 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005, pages: 296-309
• CSSV: Towards a Realistic Tool for Statically Detecting All Buffer Overflows in C Nurit Dor, Michael Rodeh, and Mooly Sagiv. PLDI 2003
• Parametric Shape Analysis via 3-Valued Logic. Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Journal ACM Transactions on Programming Languages and Systems (TOPLAS) Volume 24 Issue 3, May 2002 Pages 217 - 298
• Precise interprocedural dataflow analysis via graph reachability Reps, T., Horwitz, S., and Sagiv, M., the Twenty-Second ACM Symposium on Principles of Programming Languages, (San Francisco, CA, Jan. 23-25, 1995), pp. 49-60
• Precise interprocedural dataflow analysis with applications to constant propagation Sagiv, M., Reps, T., and Horwitz, S., . Theoretical Computer Science 167 (1996), 131-170