Hossein Hojjat

Assistant Professor
He received his Ph.D. from EPFL

Research Interests

Formal Methods

Software Verification

Analysis and Synthesis

Automated Reasoning

  • Research
  • Teaching
  • Resume

Conference Papers


  • Hossein Hojjat,Philipp Ru¨mmer, Ali Shamakhi: “On  Strings  in Software  Model Checking”, Proceedings  of the 17th Asian Symposium on Programming Languages and Systems (APLAS2019)
  • Hossein Hojjat, Philipp Ru¨mmer:  “The  Eldarica  Horn Solver”, Proceedings  of the  18th  In- ternational Conference on Formal  Methods  in Computer-Aided Design (FMCAD’18)
  • Hossein Hojjat, Philipp  Ru¨mmer:  “Deciding  and  Interpolating Algebraic  Data  Types  by Reduction”, Proceedings  of the  19th  International Symposium  on  Symbolic  and  Numeric Algorithms  for Scientific Computing (SYNASC’17)
  • Jedidiah McClurg,  Hossein  Hojjat,  Pavol  Cerny:   “Synchronization  Synthesis  for Network Programs”, Proceedings of the 29th International Conference on Computer Aided Verification (CAV’17)
  • Shrutarshi Basu, Nate Foster, Hossein Hojjat, Paparao Palacharla, Christian Skalka, Xi Wang: “Life on the Edge: Unraveling  Policies into Configurations”, Proceedings  of the ACM/IEEE Symposium on Architectures for Networking  and Communications Systems (ANCS’17)
  • Hossein Hojjat: “The FMCAD 2016 graduate student forum”, Proceedings  of the 16th Inter- national  Conference on Formal  Methods  in Computer-Aided Design (FMCAD’16)
  • Hossein Hojjat, Philipp Ru¨mmer,  Jedidiah  McClurg,  Pavol  Cerny,  Nate  Foster:   “Optimiz- ing Horn Solvers for Network  Repair”,  Proceedings  of the  16th  International Conference  on Formal  Methods  in Computer-Aided Design (FMCAD’16)
  • Jedidiah McClurg, Hossein Hojjat,  Nate  Foster,  Pavol  Cerny:  “Event-driven Network  Pro- gramming”  , Proceedings  of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’16)
  • Jedidiah McClurg, Hossein Hojjat, Pavol Cˇerny´, Nate Foster:  “Efficient Synthesis of Network Updates”, Proceedings  of the  36th  ACM SIGPLAN  Conference  on Programming Language Design and Implementation (PLDI’15)
  • Sudip Roy, Lucja  Kot,  Gabriel  Bender,  Bailu  Ding,  Hossein Hojjat,  Christoph Koch,  Nate Foster,  Johannes  Gehrke:  “The  Homeostasis  Protocol:   Avoiding  Transaction Coordination Through  Program Analysis”,  Proceedings  of the 2015 ACM SIGMOD  International  Confer- ence on Management of Data  (SIGMOD’15)


  • Hossein Hojjat, Jedidiah   McClurg,  Pavol Cˇerny´, Nate  Foster:   “Network  Updates  for the Impatient: Eliminating Unnecessary Waits”, Proceedings  of the First  Workshop  on Program- ming Languages  and Verification  Technology  for Networking  (PLVNET’15)
  • Hossein Hojjat, Philipp Ru¨mmer, Pavle Subotic, Wang Yi: “Horn Clauses for Communicating Timed Systems”,  Proceedings  of the  First  Workshop  on Horn  Clauses  for Verification  and Synthesis  (HCVS’14)
  • Philipp Ru¨mmer, Hossein Hojjat, Viktor Kuncak:  “Classifying and Solving Horn Clauses for Verification”,  Proceedings  of the 5th International Conference on Verified Software:  Theories, Tools, Experiments (VSTTE’13)
  • Philipp Ru¨mmer, Hossein Hojjat, Viktor Kuncak:  “Disjunctive Interpolants for Horn-Clause Verification”,  Proceedings  of the 25th International Conference on Computer Aided Verifica- tion (CAV’13)
  • Hossein Hojjat, Radu Iosif, Filip  Koneˇcny´, Viktor  Kuncak  and  Philipp  Ru¨mmer:  “Acceler- ating  Interpolants”, Proceedings  of the  10th  International Symposium  on Automated Tech- nology for Verification  and Analysis (ATVA’12)
  • Hossein Hojjat, Filip  Koneˇcny´,  Florent Garnier,   Radu  Iosif,  Viktor  Kuncak  and  Philipp Ru¨mmer:  “Verification  Toolkit  for Numerical  Transition Systems (tool paper)”, Proceedings of the 18th International Symposium on Formal  Methods  (FM’12)
  • Bahman Pourvatan, Marjan Sirjani,  Hossein Hojjat  and  Farhad Arbab:   “Analysis  of Reo Circuits  using Symbolic Execution”, Proceedings  of the  8th  International Workshop  on the Foundations of Coordination Languages  and Software Architectures (FOCLASA’09)
  • Hossein Hojjat, Mohammad Reza Mousavi,  Marjan  Sirjani:  “Process  Algebraic  Verification of SystemC  Codes”, Proceedings  of the 8th International Conference on Application  of Con- currency  to System Design (ACSD’08)
  • Hossein Hojjat, Mohammad Reza Mousavi,  Marjan  Sirjani:  “A Framework  for Performance Evaluation and  Verification  in Stochastic  Process  Algebras”,  Proceedings  of the  22nd ACM Symposium on Applied Computing, Software Verification  Track  (SV’08)
  • Hossein Hojjat, Marjan Sirjani,  Mohammad  Reza Mousavi and Jan  Friso Groote:  “Sarir:  A Rebeca to  mCRL2  Translator”, Proceedings  of the  7th  IEEE  International Conference  on Application  of Concurrency to System Design (ACSD’07)
  • Fahimeh Raja ,  Hadi  Amiri  ,  Samira  Tasharofi,   Hossein  Hojjat  and  Farhad Oroumchian: “Evaluation of part  of speech tagging on Persian  text”, Proceedings  of the Second Workshop on Computational Approaches  to Arabic Script-based Languages  (CAASL2’07)
  • Hadi Amiri, Hosein Hojjat,  Farhad  Oroumchian: “Investigation on a Feasible  Corpus  For Persian  POS  Tagging”  (in  Persian), Proceedings  of the  12th  International CSI  Computer Conference (CSICC’07)
  • Hossein Hojjat, Hootan Nakhost,  Marjan  Sirjani:  “Formal  Verification  of the  IEEE  802.1D Spanning Tree Protocol  Using Extended Rebeca”, Proceedings  of the First  IPM International Workshop  on Foundations of Software Engineering  (FSEN’05)

Journal Papers


  • Philipp Ru¨mmer, Hossein Hojjat, Viktor Kuncak:  “On recursion-free Horn clauses and Craig interpolation”, Formal  Methods  in System Design, v.47, n.  1, pp.  1-25, 2015.
  • Bahman Pourvatan, Marjan Sirjani, Hossein Hojjat and Farhad Arbab:  “Symbolic Execution of Reo Circuits  using Constraint Automata”, Science of Computer Programming, Elsevier, v.77, n.  7-8, pp.  848-869, 2012.
  • Hossein Hojjat, Mohammad Reza  Mousavi,  Marjan  Sirjani:   “Formal  Analysis  of SystemC Designs in Process Algebra”,  Fundamenta Informaticae, v. 107, n.  1, pp.  19-42, 2011.
  • Hossein Hojjat, Hootan Nakhost,  Marjan  Sirjani:  “Integrating Module Checking and Deduc- tion  in a Formal  Proof  for the  Perlman Spanning  Tree  Protocol  (STP)”, J.UCS  Journal of Universal  Computer Science, v. 13, n.  13, pp.  2076-2104, 2007.

Technical Reports


  • Jedidiah McClurg, Hossein Hojjat, Nate Foster,  Pavol Cˇerny´:  “Specification and Compilation of Event-driven SDN Programs”, CoRR abs/1507.07049, 2015.
  • Hossein Hojjat, Philipp Ru¨mmer, Pavle  Subotic,  Wang  Yi:  “Uniform  Analysis  for Commu- nicating  Timed  Systems (Extended Technical  Report)”, EPFL-REPORT-190680, 2013.
  • Hossein Hojjat, Mohammad  Reza  Mousavi  Mousavi,  Marjan  Sirjani:   “Application of pro- cess algebraic  verification  and reduction techniques  to SystemC  designs”,  Computer Science Report  No. 08-15, Technische  Universiteit Eindhoven,  2008.
  • Farhad Oroumchian, Samira Tasharofi, Hadi Amiri, Hossein Hojjat, Fahimeh Raja:  “Creating a Feasible Corpus for Persian POS Tagging”,  Technical Report Number TR 3/2006, University of Wollongong in Dubai,  2006.


  • Programming Languages and Compilers: Fall 2018, Spring 2019, University of Tehran.
  • Programming Language Concepts (CSCI-344):  Fall 2016, Rochester Institute of Technology.
  • Theory of Computation: Fall 2019, University of Tehran.


  • Compiler Construction (CSCI-742): Spring 2017, Spring 2018, Rochester Institute of Technology.
  • Programming Language Theory (CSCI-740):  Fall 2017, Rochester Institute of Technology.
  • Introduction to Formal Methods  (with  Fatemeh Ghassemi):  Fall 2018, Fall 2019, University of Tehran.
  • Software Synthesis: Spring 2019, University of Tehran.


M.S., University of Tehran

B.Sc., University of Tehran