Safe and Smart Software (S3) Lab
research interests span the areas of formal methods and concurrent and
distributed computing. We develop specification, verification and
synthesis techniques and tools to build reliable, secure and efficient
computing systems, in particular, subtle concurrent and distributed
systems. We often reduce verification and synthesis to simple
sufficient conditions to leverage the increasingly powerful automated
and semi-automated reasoning techniques and tools.
Here is my research statement. Here are some of our current and past projects:
- Automatic analysis and synthesis of distributed systems POPL'19, CAV'20
- Verification of distributed systems POPL'16, ICFP'20
- Blockchain transactions ICBC'20
- Automatic fence insertion OOPSLA'15, PODC'17, DISC'19
- Learning performance models MAPL'20
- Domain-specific languages and type systems OOPSLA'18
- Concurrency Programming models, Testing and Verificaiton PPoPP'11, CONCUR'12, CAV'14, DISC'13, DISC'14, NFM'19
Our research has been recognized as SIGPLAN Research Highlight in 2019
and received the distinguished paper award at OOPSLA 2018.
Jeremiah Griffin (undergraduate)
Xiao Li (masters)
Dynamic Point: Gradually Precise Types for Numerical Analysis
Joseph Tarango, Mohsen Lesani, Philip Brisk
Grafs: Graph Analytics Fusion and Synthesis
Farzin Houshmand, Mohsen Lesani, Keval Vora
Verified Transactions From Verified Linearizable Objects, Modularly
Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J Bell, Adam Chlipala, Benjamin C. Pierce, Steve Zdancewic
Hampa: Solver-aided Recency-Aware Replication
Xiao Li, Farzin Houshmand, Mohsen Lesani
CAV'20 (International Conference on Computer-Aided Verification)
TLC: Temporal Logic of Distributed Components
Jeremiah Griffin, Mohsen Lesani, Narges Shadab, Xizhe Yin
ICFP'20 (ACM SIGPLAN International Conference on Functional Programming)
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)
Narges Shadab, Farzin Houshmand, Mohsen Lesani
ICBC'20 (IEEE International Conference on Blockchain and Cryptocurrency)
Learning Quantitative Representation Synthesis
Mayur Patil, Farzin Houshmand, Mohsen Lesani
MAPL'20 (ACM Machine Learning and Programming Languages Workshop)
Coordination Analysis and Synthesis
Farzin Hooshmand, Mohsen Lesani
POPL'19 (ACM Principles of
Polynomial-time Fence Insertion For Structured Programs
Mohammad Taheri, Arash Pourdamghani, Mohsen Lesani
DISC'19 (The International Symposium on Distributed Computing)
Transaction Protocol Verification with Labeled Synchronization Logic
NFM'19 (NASA Formal Methods Symposium)
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,
ACM SIGPLAN highlight
Invitied to Communications of ACM
The rest of publications
Analysis and Synthesis
Replicated systems are widely deployed to tolerate faults in aviation
control systems and geo-distributed data stores. Given high-level sequential specifications, we automatically analyze
the specifications and synthesize convergent, consistent, recent, and coordination-avoiding replicated distributed systems.
See the POPL'19 paper
and CAV20 paper
Certified Key-value Stores
We implement, specify and mechanically verify distributed key-value
stores in proof assistants.
See the POPL'16 paper
Compositional Verification of Distributed System Stacks
What are the fundamental principles for compositional verification of
distributed systems? We design program logics and compositional
verification techniques to build certified distributed system stacks.
See the ICFP paper
Ongoing project: Automatic
Synthesis of Parallel and Distributed Graph-processing
Given a high-level specification of a graph processing problem, we
automatically synthesize programs for multiple parallel and distributed
Blockchains and Cryptocurrencies
How can we atomically exchange assets across multiple
See the ICBC'20
project: Certified Blockchains with Explicit Safety and Security Guarantees
What are the correctness conditions
and verification principles for blockchain
protocols? We aim at building certified blockchains with explicit safety and
security guarantees using proof assistants.
Transaction Specification, Testing and Verification
What are the correctness criteria
and proof techniques for transactions?
the DISC'14, WTTM'12 and WTTM'13 papers.
We presented a testing technique
that found bugs in transaction algorithms.
See the DISC'13 paper.
We have built a mechanically
checked framework for verification of transactional
See the CONCUR'12 paper.
specify and implement
safe transactions in the presence of communication between them.
See the PPoPP'12 paper.
To gain performance, compilers and processors reorder
program instructions. Reordering instructions may violate
safety of concurrent executions. Experts insert fence
instructions to prevent violating reorders. We automate fence insertion.
See the OOPSLA'15 paper
and PODC'17 paper and DISC'19 paper.
of Concurrent Data
Composing atomic concurrent
operations is challenging and researchers have found a myriad of atomicity bugs in compositions of concurrent
libraries. We automatically verify the
atomicity of compositions.
See the CAV'14 paper.
Composable Concurrent Programming
We are building a certified
concurrent collections library that
supports atomic composition of method calls across objects.
Trust and Security
Ongoing project: Memory safety
attackers can use out-of-bound memory
accesses to take over the whole
system. We develop static and dynamic techniques to ensure that memory
accesses are within bounds and within the access capabilities of the enclosing module.
See our NSF-supported project.
for Secure Cloud Computations
To protect user privacy, we
encrypt data before processing it in the
cloud. We apply type inference to find the most efficient encryption
See the OOPSLA'13 paper.
Aggregation and Inference in Social Networks
Given local trust
information between direct friends, we automatically infer a trust
measure between any pair of users.
See the JCI'09 paper
Performance Models to Guide
Synthesis of Efficient Concurrent Data Structures
a high-level relational specification of
data, we automatically synthesize efficient concurrent data
structures. Performance is an irregular phenomenon that can be only
learned from experiments. We train neural networks as performance
models. We use the performance model to choose the most efficient
candidate from the space of possible candidate data structures.
See the MAPL'20 paper.
between Q-Learning Agents
We presented a
technique for cooperation between heterogeneous Q-learning agents.
See the SMC'04 paper.
Language and Type System for Programming Biochemistry
We introduce the BioScript domain-specific language for programmable
biochemistry which executes on emerging microfluidic platforms and the
ChemType type system that ensures that the chemical interactions are
See the OOPSLA'18 paper
Ongoing project: Drug Synthesis
Can we apply program synthesis techniques to
automatically synthesize drugs with specified properties?
SHF CRII: Certified Byzantine Fault-tolerant Systems. M Lesani. 2017-2019
NSF SaTC: Practical Whole Kernel Memory Safety Enforcement. C.
Song, M. Lesani. 2017-2020
NSF FET: Stochastic Synthesis of Peptides and Small Molecules. M. Lesani, P. Brisk, W. Grover. 2019-2022.
NSF CAREER: Distributed System Synthesis on Certified Middleware. M. Lesani. 2020-2025