Courses (2012-2013)

• 0368.3133 (Oct'12): Compilation Course.
• 0368.405101 (Oct'12): Program Analysis.
• (February'13): A workshop on using data structure synthesis (jointly with Shachar Itzhaky)

Research

My research focuses broadly on easing the task of developing reliable and efficient 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.

Current Grants

• 2013-18 Verifying and Synthesizing Software Compositions, ERC advanced grant
  
  We are looking for outstanding students with a solid background in programming languages, formal methods, and algorithms. Positions are available for PhD and postdoctoral studies. Only top students
  will be considered.
• 2011-15 Enabling Software Scalability via Dynamic and Static Program Analysis Israel Science Foundation

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 [.ppt], [.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, December 2012.
• Concurrent Libraries with Foresight. Guy Golan Gueta, G. Ramalingam, Mooly Sagiv, and Eran Yahav. To appear in PLDI'2013
• Synthesis of Circular Compositional Program Proofs via Abduction. Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, and Mooly Sagiv. To appear in TACAS'13
• 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, 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 (PLDI'12). (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 2012.
• Eventually Consistent Transactions. Sebastian Burckhardt, Manuel Fahndrich, Daan Leijen, and Mooly Sagiv Proceedings of the European Symposium on Programming, 2012. full version
• 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 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 2011
• Data Representation Synthesis. P. Hawkins, A. Aiken, K. Fisher, and M. Sagiv. Proceedings of the Conference on Programming Language Design and Implementation 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. 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 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 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
• 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
• 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
• Speeding up slicing. T. Reps, S. Horwitz, M. Sagiv, M., and G. Rosay. In SIGSOFT '94: Proceedings of the Second ACM SIGSOFT Symposium on the Foundations of Software Engineering (Awarded an ACM SIGSOFT Retrospective Impact Paper Award 2011.)