Research Statement

My main research interest is on Program Analysis and Verification. In general, I am interested on applying static program analysis techniques for inferring runtime program properties. So far, I have focused on inferring complexity bounds of sequential imperative programs:

  • I have developed techniques for inferring precise worst-case and best-case complexity bounds
  • The applied techniques are based of symbolic computation and static analysis

I also have obtained some theoretical complexity results (together with my co-authors) on the termination property of some simple loops. Mainly, I have shown that

  • Termination of some simple loops are undecidable
  • Termination of some other simple loops have EXPSPACE-hard lower bound

At present, I am working on the expressiveness of some abstract program models with respect to some program properties, trying to understand the theoretical limits of the respective models and possible minimal extensions of these models in obtaining sound and precise program properties. I am also interested on program termination, and algorithmic verification of concurrent programs. More information can be found in my research statement.

Research Interest

Program Analysis, Static Analysis, Termination, Software Verification, Abstract Interpretation, Program Synthesis, Theorem proving, Program Semantics

My Limited Publication List

  • Elvira Albert, Samir Genaim, and Abu Naser Masud.On the inference of resource usage upper and lower bounds. ACM Transactions on Computational Logic, 2013. To appear.
  • Amir M. Ben-Amram, Samir Genaim, and Abu Naser Masud. On the termination of integer loops. ACM Trans. Program. Lang. Syst., 34(4):17, 2012.
  • Amir M. Ben-Amram, Samir Genaim, and Abu Naser Masud. On the termination of integer loops. In Viktor Kuncak and Andrey Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Philadelphia, USA, January 25-27, 2012. Proceedings, volume 7148 of Lecture Notes in Computer Science, pages 72-87. Springer, January 2012.
  • Elvira Albert, Samir Genaim, and Abu Naser Masud. More precise yet widely applicable cost analysis. In Ranjit Jhala and David A. Schmidt, editors, Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings, volume 6538 of Lecture Notes in Computer Science, pages 38-53. Springer, January 2011.

Theses

  • Termination and Cost Analysis: Complexity and Precision Issues. PhD thesis, School of Computer Science, Technical University of Madrid,Spain, February 2013, Advisor: Samir Genaim and German Puebla.
  • Minimization methods for exogenous coordination models. MSc thesis, International Center for Computational Logic, Department of Computer Science, University of Technology Dresden, Germany, March 2009, Advisor: Prof. Christel Baier.

Quick Links

Recent News