Mohsen Lesani
Assistant Professor
Computer Science and Engineering Department
University of California, Riverside

      Winston Chung Hall 312

Mailing Address:
      900 University Avenue,
      Winston Chung Hall 351
      Riverside, CA 92521

      LastName AT cs.ucr.edu
Mohsen Lesani


 Bio Sketch

  I am an assistant professor at the Computer Science and Engineering Department of the University of California, Riverside.

The overarching goal of my research is to make computing systems more reliable and efficient. I am broadly interested in both formal methods, and concurrent and distributed computing. I apply program analysis and verification techniques to specify, verify and synthesize concurrent and distributed systems. I am also interested in concurrent and distributed programming models and consistency conditions.

I spent my postdoc at MIT and obtained my PhD from UCLA. I obtained my BS and MS from the University of Tehran and Sharif University of Technology. I have research experience with Scalable Synchronization Lab at Oracle (Sun) Labs and HP Labs.

Some of my ongoing projects are
▸ Program Logics and Compositional Verification for Distributed System Stacks
▸ Certified Blockchains with Explicit Safety Guarantees
▸ Coordination Analysis and Synthesis of Replicated Data Types
▸ Learning Performance Models to Guide Synthesis of Efficient Concurrent Data Structures
▸ Automatic Synthesis of Parallel and Distributed Graph-processing Programs
▸ Certified Composable Concurrent Programming
▸ Language and Type System Design for Programmable Biochemistry
▸ Spacial Memory Safety
▸ ...

Prospective Students



BioScript: Programming Safe Chemistry of Laboratories-on-a-Chip
Jason Ott, Chris Curtis, Tyson Loveless, Mohsen Lesani, Philip Brisk
OOPSLA'18 (ACM Object-oriented Programming, Systems, Languages, and Applications)

Brief Announcement: Fence Insertion for Straight-line Programs is in P
Mohsen Lesani
PODC'17 (ACM Symposium on Principles of Distributed Computing)
[Paper] More

Chapar: Certified Causally Consistent Distributed Key-Value Stores
Mohsen Lesani, Christian J. Bell, Adam Chlipala
POPL'16 (ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages)
[Paper] More

Declarative Fence Insertion
John Bender, Mohsen Lesani, Jens Palsberg
OOPSLA'15 (ACM Object-oriented Programming, Systems, Languages, and Applications)
[Paper] More

AtomChase: Directed Search towards Atomicity Violations
Mahdi Eslamimehr, Mohsen Lesani
ISSRE'15 (IEEE International Symposium on Software Reliability Engineering)
Best paper award

Decomposing Opacity
Mohsen Lesani, Jens Palsberg
DISC'14 (International Symposium on DIStributed Computing), WTTM'13
[Paper] More

Automatic Atomicity Verification for Clients of Concurrent Data Structures
Mohsen Lesani, Todd Millstein, Jens Palsberg
CAV'14 (International Conference on Computer Aided Verification)
[Paper] More

On the Correctness of Transactional Memory Algorithms
Mohsen Lesani
PhD Dissertation
[Dissertation] More

MrCrypt: Static Analysis for Secure Cloud Computations
Sai Deep Tetali, Mohsen Lesani, Rupak Majumdar, Todd Millstein
OOPSLA'13 (ACM Object-oriented Programming, Systems, Languages, and Applications)
[Paper] More

Proving Non-opacity
Mohsen Lesani, Jens Palsberg
DISC'13 (International Symposium on DIStributed Computing), Transact'13
[Paper] More

A Framework for Formally Verifying Software Transactional Memory Algorithms
Mohsen Lesani, Victor Luchangco, Mark Moir
CONCUR'12  (International Conference on Concurrency Theory)
[Paper] More

Communicating Memory Transactions
Mohsen Lesani, Jens Palsberg
PPoPP'11 (ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming)

Semantics-preserving Sharing Actors
AGERE'13 (ACM Workshop on Programming based on Actors, Agents, and Decentralized Control)
Mohsen Lesani, Antonio Lain
[Paper] More

Specifying Transactional Memories with Nontransactional Operations
WTTM'13  (Workshop on the Theory of Transactional Memory)
Mohsen Lesani, Victor Luchangco, Mark Moir

Putting Opacity in its Place
Mohsen Lesani, Victor Luchangco, Mark Moir
WTTM'12  (Workshop on the Theory of Transactional Memory)

Fuzzy Trust Aggregation And Personalized Trust Inference In Virtual Social Networks
Mohsen Lesani, Niloufar Montazeri
Journal of Computational Intelligence 25/2, 2009

Aria Language, Towards Agent Orientation Paradigm
Mohsen Lesani, Niloufar Montazeri
ICSOFT'08 (International Joint conference on Software Technologies)

Successful Cooperation between Heterogeneous Fuzzy Q-Learning Agents
Ali Akhavan Bitaghsir, Amir Moghimi, Mohsen Lesani, Mohammad Mehdi Keramati, Majid Nili Ahmadabadi, Babak Nadjar Arabi
SMC'04 (IEEE International Conference on Systems, Man, and Cybernetics)

The rest of papers

 Recent Service

ECOOP'18, PC (European Conference on Object-Oriented Programming, Program Committee)
POPL'17, ERC (Principles of Programming Languages 2017, External Review Committee)
CPP'17, PC (Certified Programs and Proofs 2017, Program Committee)


NSF SHF CRII: Certified Byzantine Fault-tolerant Systems. Mohsen Lesani. 2017-2019
NSF SaTC: Practical Whole Kernel Memory Safety Enforcement. Chengyu Song, Mohsen Lesani. 2017-2020


Jeremiah Griffin
Farzin Hooshmand
Mayur Patil
Narges Shadab


  CS 179E: Project in Compilers  Spring 2017
CS 246: Advanced Verification Techniques  Winter 2017  Spring 2018
CS 260: Seminar in Program Synthesis  Fall 2017



I am from the beautiful city of Kerman where the Prince's Garden [1, 2] is located.
My PhD hooding at UCLA.
I tried acting and played John J. Astor in Titanic the musical
. Can you find me in the cast?
Niloofar and I won the best costume award in a Halloween party at MIT.