Home
 


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

Office:
      Winston Chung Hall 325

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

Email:
      LastName AT cs.ucr.edu
Mohsen Lesani

I have positions for motivated students. I will be glad to hear about your interests and accomplishments.


 
 Bio Sketch
 
I am an associate professor at the Computer Science and Engineering Department of the University of California, Riverside. Before joining UCR, I was a postdoc at MIT and obtained my PhD from UCLA. My research interests are reliability and security of software systems especially concurrent and distributed systems. I received the NSF CAREER award in 2020. My research has been recognized as SIGPLAN Research Highlight in 2019 and received the distinguished paper award at OOPSLA 2018. Here are some of our current and past projects:

- Secure and resilient information flow
      S&P'22
- Data analytics
      ICFP'21
- Blockchain transactions
      ICBC'20PODC'21
- Automatic analysis and synthesis of distributed systems
      POPL'19CAV'20
- Verification of distributed systems
      POPL'16ICFP'20
- Machine learning for performance models
      MAPL'20
- Domain-specific languages and type systems
      OOPSLA'18CACM'21
- Automatic fence insertion for concurrent systems
      OOPSLA'15PODC'17DISC'19
- Concurrency programming models, testing and verificaiton
     PPoPP'11CONCUR'12DISC'13DISC'14CAV'14NFM'19

 
 Papers


Modular Mechanized Verification of Transactional Predication
Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J Bell, Adam Chlipala, Benjamin C. Pierce, Steve Zdancewic
Submitted.

Hamraz: Resilient Object Partitioning and Replication
Xiao Li, Farzin Houshmand, Mohsen Lesani
S&P'22 (IEEE Symposium on Security and Privacy)

Grafs: Declarative Graph Analytics
Farzin Houshmand, Mohsen Lesani, Keval Vora
ICFP'21 (ACM SIGPLAN International Conference on Functional Programming)
[Paper] More

Brief Announcement: Brokering with Hashed Timelock Contracts is NP-Hard
Eric Chan, Mohsen Lesani
PODC'21 (ACM Symposium on Principles of Distributed Computing)
[Paper] More

BioScript: programming safe chemistry on laboratories-on-a-chip
Jason Ott, Tyson Loveless, Chris Curtis, Mohsen Lesani, and Philip Brisk. 2021.
CACM'21 (Communications of the ACM 64, 2, February 2021)
[Paper]

TLC: Temporal Logic of Distributed Components
Jeremiah Griffin, Mohsen Lesani, Narges Shadab, Xizhe Yin
ICFP'20 (ACM SIGPLAN International Conference on Functional Programming)
[Paper] More

Hampa: Solver-aided Recency-Aware Replication
Xiao Li, Farzin Houshmand, Mohsen Lesani
CAV'20 (International Conference on Computer-Aided Verification)
[Paper] More

UBITect: A Precise and Scalable Method to Detect Use-Before-Initialization bugs in Linux Kernel
Y. Zhai, Y. Hao, H. Zhang, D. Wang, C. Song, Z. Qian, M. Lesani, S. Krishnamurthy, P. Yu
ESEC/FSE'20 (The ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering)
[Paper] More

Cross-Chain Transactions
Narges Shadab, Farzin Houshmand, Mohsen Lesani
ICBC'20 (IEEE International Conference on Blockchain and Cryptocurrency)
[Paper] More

Learning Quantitative Representation Synthesis
Mayur Patil, Farzin Houshmand, Mohsen Lesani
MAPL'20 (ACM SIGPLAN Machine Learning and Programming Languages Workshop)
[Paper] More

Hamsaz: Replication Coordination Analysis and Synthesis
Farzin Houshmand, Mohsen Lesani
POPL'19 (ACM SIGPLAN Symposium on Principles of Programming Languages)
[Paper] More

Polynomial-time Fence Insertion For Structured Programs
Mohammad Taheri, Arash Pourdamghani, Mohsen Lesani
DISC'19 (The International Symposium on Distributed Computing)
[Paper] More

Transaction Protocol Verification with Labeled Synchronization Logic
Mohsen Lesani
NFM'19 (NASA Formal Methods Symposium)
[Paper] More

BioScript: Programming Safe Chemistry of Laboratories-on-a-Chip
Jason Ott, Chris Curtis, Tyson Loveless, Mohsen Lesani, Philip Brisk
OOPSLA'18 (ACM SIGPLAN conference on Object-oriented Programming, Systems, Languages, and Applications)
Distinguished paper award
SIGPLAN Research Highlight 2019
Invited to Communications of ACM
[Paper] More

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 Symposium on Principles of Programming Languages)
[Paper] More

Declarative Fence Insertion
John Bender, Mohsen Lesani, Jens Palsberg
OOPSLA'15 (ACM SIGPLAN conference on 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
More

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 SIGPLAN conference on 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 Principles and Practice of Parallel Programming)
[Paper]

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
[Paper]

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

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

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

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)
[Paper]


The rest of papers



 Service


OOPSLA'21, PC (ACM Object-oriented Programming, Systems, Languages, and Applications, Program Committee)

OOPSLA'20, PC (ACM Object-oriented Programming, Systems, Languages, and Applications, Program Committee)

DisCoTec'20, PC (International Federated Conference on Distributed Computing Techniques, P
rogram Committee)

POPL'20, PC (ACM Principles of Programming Languages, Program Committee)

ECOOP'18, PC (European Conference on Object-Oriented Programming, Program Committee)

NSF Panel 2018


POPL'17, ERC (ACM Principles of Programming Languages 2017, External Review Committee)


CPP'17, PC (ACM Certified Programs and Proofs 2017, Program Committee)


 Grants


NSF CAREER: Distributed System Synthesis on Certified Middleware. M. Lesani. 2020-2025

NSF FET: Stochastic Synthesis of Peptides and Small Molecules. M. Lesani, P. Brisk, W. Grover. 2019-2022.


NSF SaTC: Practical Whole Kernel Memory Safety Enforcement. C. Song, M. Lesani. 2017-2020

NSF SHF CRII: Certified Byzantine Fault-tolerant Systems. M. Lesani.
2017-2019


 Students


Eric Chan
Farzin Hooshmand
Xiao Li
Javad Saber-Latibari
Gregory Shar

Graduated students:
   Xiao Li (masters), Now my PhD student
   Paranshu Singhal (masters), Now at Amazon AWS
   Jeremiah Griffin (undergraduate), Now at Garmin International


 Teaching
 
CS 160: Concurrent Programming and Parallel Systems
   F'20, F'19

CS 179E: Project in Computer Science
   Su'21, W'21, Su'20, W'20, W'19, S'17

CS 247: Principles of Distributed Computing  
   S'20

CS 246: Software Verification
   S'21, S'18, W'17

CS 260: Seminar in Program Synthesis
   F'17

CS 260: Seminar in Distributed Computing
   S'19

 
 Other


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?
We won the best costume award in a Halloween party at MIT.
I try to keep the positive feedbacks that we get.