Alan Smith

Mohammad Esmail Esmaili

Software Engineer

Personal Profile

I recently graduated with a M.Sc degree in Computer Software Engineering, at Sharif University of Technology under directly supervision of Prof. Ali Movaghar . I am enthusiastically interested in Formal Verification specially, Model Checking, fields.


Master of Software Engineering

Sharif University of Technology, Tehran, Iran(2012-2014)

GPA: 17.1 (out of 20)

Thesis: "Model Checking of Priced Timed Activity Networks (PTAN)"

Bachelor of Software Engineering

University of Science and Culture, Tehran, Iran(2006-2011)

GPA: 16 (out of 20)

Interseted Fields

  • Formal Verification

  • Model Checking

  • Automata and language

  • Logics

  • Distributed Systems and Algorithms


  1. Mohammad Esmail Esmaili, Reza Entezari Maleki, Ali Movaghar,'Improved Region Based TCTL Model Checking of Timed Petri Nets',to appear in The Journal of Computing Science and Engineering (JCSE).

  2. Draft Available : Mohammad Esmail Esmaili, Ali Movaghar, 'Priced Timed Activity Networks'.

Teaching Experience

  • Teaching assistant for Design and Implementation of Programming Languages at University of Science and Culture (2011).

  • Teaching assistant for Verification of Reactive Systems at Sharif University of Technology.(2014)

Research Experience

Model checking

2013 - Present

Modeling some real times models by Timed Automata(TA) and Time Petri Net(TPN) in several tools such as UPPAAL, KRONOS, Romeo and Tina and then verify considered properties of these systems in mentioned tools.

Distributed Algorithms

2012 - 2012

We prepared a survey in the field of Leader election for Mobile Ad hoc Networks. In this work, we study an overview of algorithms that is introduced for Leader Election problem for Mobile Ad hoc Network that is compatible with node mobility and dynamic Topology changes.

Image processing

2011 - 2012

we attempt to control the traffic light by approximating the number of cars for change traffic light by use image processing algorithms under supervision of Prof. Balafar at University of Tabriz; that resulted research caused to it implemented in MATLB.


2011 - 2012

Concurrency Control in Distributed Database. In this research, after an overview on prevalent concurrency control on centralized Database; we introduced most important techniques that are proposed to perform concurrency control on distributed Database.

Computer Skills

  • Model checking Tools: UPPAAL, Tina, SAN, Romeo, UPPAAL CORA, Kronos, PRISM
  • Prgoramming: C/C++, MATLAB, C#, Java
  • Graphic: Adobe Photoshop, CorelDraw, Freehand
  • Operating Systems: Windows, Linux, FreeBSD
  • Web Design: HTML, CSS, JavaScript, ASP
  • Other Major Softwares: Microsoft Visual Studio, Microsoft Office, Adobe Dreamweaver, Mobius

Language Skills

  • English: good
  • Persian: Native
  • Azerbaijani: good
  • Arabic: familiar


Performance and Dependability Laboratory (PDL), Department of Computer Engineering, Sharif University of Technology (2012-Present).

Free counter and web stats