I am a PhD student at the Embedded Systems Lab (ESLAB) in Linköping University. Currently I do research on the formal verification of multi-threaded programs. My supervisors are Prof. Zebo Peng, Prof. Petru Eles and Dr. Ahmed Rezine.

Publications:

  1. Zeinab Ganjei, Ahmed Rezine, Petru Eles and Zebo Peng
    Lazy Constrained Monotonic Abstraction
    To appear in Verification, Model Checking, and Abstract Interpretation {VMCAI} 2016.
  2. Zeinab Ganjei, Ahmed Rezine, Petru Eles and Zebo Peng
    Dynamically Counting Synchronizing Processes
    To appear in International Journal on Software Tools for Technology Transfer {STTT}.
  3. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Zeinab Ganjei, Ahmed Rezine and Yunyun Zhu
    Verification of Cache Coherence Protocols wrt. Trace Filters
    Proceedings of Formal Methods in Computer-aided Design {FMCAD} 2015, Austin, Texas, USA.
  4. Zeinab Ganjei, Ahmed Rezine, Petru Eles and Zebo Peng
    Abstracting and Counting Synchronizing Processes
    Proceedings of Verification, Model Checking, and Abstract Interpretation - 16th International
    Conference, {VMCAI} 2015, Mumbai, India.
  5. Mohammad Ali Hadavi, Ernesto Damiani, Rasool Jalili, Stelvio Cimato and Zeinab Ganjei
    AS5: A Secure Searchable Secret Sharing Scheme for Privacy Preserving Database Outsourcing
    Data Privacy Management and Autonomous Spontaneous Security, 7th International
    Workshop, {DPM} 2012, Pisa, Italy.

Tools:

  1. PACMAN: (PredicAted Constrained Monotonic AbstractioN) A verification tool that performs parameterized verification for programs whose correctness crucially depends on precisely capturing the effect shared variables or barriers have on the synchronization among the threads.
    Source Code
    Cite: bibtex
    Zeinab Ganjei, Ahmed Rezine, Petru Eles and Zebo Peng
    Abstracting and Counting Synchronizing Processes
    Proceedings of Verification, Model Checking, and Abstract Interpretation - 16th International
    Conference, {VMCAI} 2015, Mumbai, India.
  2. ZAAMA: A tool that implements constrained monotonic abstraction.
    Source Code
    Cite: bibtex
    Zeinab Ganjei, Ahmed Rezine, Petru Eles and Zebo Peng
    Abstracting and Counting Synchronizing Processes
    Proceedings of Verification, Model Checking, and Abstract Interpretation - 16th International
    Conference, {VMCAI} 2015, Mumbai, India.
    Parosh Aziz Abdulla, Yu-Fang Chen, Giorgio Delzanno, Frédéric Haziza, Chih-Duo Hong, Ahmed Rezine
    Constrained Monotonic Abstraction: A CEGAR for Parameterized Verification
    Proceedings of the 21st International Conference on Concurrency Theory {CONCUR} 2010