# Publications Source: https://ranadeep.in/publications.md --- layout: default title: "Publications" permalink: /publications --- - ### On the Complexity of Checking Consistency for Replicated Data Types. with [Constantin Enea][cenea] and [Michael Emmi][memmi]: [CAV 2019](https://link.springer.com/chapter/10.1007%2F978-3-030-25543-5_19) - ### Checking Causal Consistency of Distributed Databases. with Rachid Zennou, [Ahmed Bouajjani][abou], [Constantin Enea][cenea] and Mohammed Erradi: [NETYS 2019](https://link.springer.com/chapter/10.1007%2F978-3-030-31277-0_3) - ### On the complexity of checking transactional consistency. with [Constantin Enea][cenea]: [OOPSLA 2019](https://dl.acm.org/doi/10.1145/3360591) - ### MonkeyDB: Effectively Testing Correctness against Weak Isolation Levels. with Diptanshu Kakwani, Jyothi Vedurada, [Constantin Enea][cenea], [Akash Lal][alal]: [OOPSLA 2021](https://dl.acm.org/doi/10.1145/3485546) [[OOPSLA artifact](https://zenodo.org/record/5530883), [Microsoft repository](https://github.com/microsoft/weak-isolation-mock-db)] [cenea]: https://www.irif.fr/~cenea [memmi]: https://michael-emmi.github.io [alal]: https://www.microsoft.com/en-us/research/people/akashl [abou]: https://www.irif.fr/~abou --- # Homepage Source: https://ranadeep.in/index.md --- # You don't need to edit this file, it's empty on purpose. # Edit whiteglass' home layout instead if you want to make some changes. # See: https://jekyllrb.com/docs/themes/#overriding-theme-defaults layout: home title: "Homepage" --- I am currently seeking research and engineering roles in formal methods. I focus on automated verification, specification languages, [model checking][model-checking], and developer-facing tools for safety-critical software. I am also interested in projects at the intersection of AI and formal methods, including AI-assisted specification and verification tools, and formal methods for specifying, verifying, and evaluating AI-agent behavior. Until April 2026, I built production blockchain infrastructure at [Informal Systems][informal]. Most recently, I was part of the team developing [Emerald][emerald], a modular framework for institutional blockchains. Emerald uses [EVM][evm] with [Solidity][solidity] contracts on top of consensus engines like [Malachite][malachite] and [Commonware Simplex][simplex]. I previously developed [Inter-Blockchain Communication][ibc] in [Rust][rust] and [Cairo][cairo] ([Starknet][starknet]), and conducted security audits for [Cosmos SDK][cosmos-sdk], [Tendermint][tendermint], [IBC][ibc], and [CosmWasm][cosmwasm] smart contracts. My applied work combines protocol engineering, automated testing, and security audits for distributed systems. In that work, I developed [model-based testing][model-based-testing] tooling for audits and internal software development, using [TLA+][tla] specifications and [model checking][model-checking] to compare implementations against their specifications and uncover protocol correctness issues. My formal methods background comes from my Ph.D. in Computer Science at [Université Paris Cité][u-paris] (formerly Université de Paris), where I worked in the [Modeling and verification][verif] team at [IRIF][irif] under [Prof. Constantin Enea][cenea]. My thesis focused on automated formal testing of distributed databases, leading to [4 publications](/publications) on this topic. I [defended it on March 30, 2021][defense]. My B.Sc. and M.Sc. in Computer Science are from [Chennai Mathematical Institute][cmi]. For my detailed experience and career history, see my CV: [ranadeep_cv.pdf][cv-pdf]. [cenea]: http://www.lix.polytechnique.fr/~cenea [verif]: https://www.irif.fr/en/equipes/verif/index [irif]: https://www.irif.fr [cmi]: https://www.cmi.ac.in [cv-pdf]: /ranadeep_cv.pdf [defense]: /defense [informal]: https://informal.systems [u-paris]: https://u-paris.fr/language/en/ [ibc]: https://ibc.cosmos.network/main/ibc/overview.html [cairo]: https://www.cairo-lang.org [starknet]: https://starknet.io [rust]: https://www.rust-lang.org [emerald]: https://informal.systems/emerald [evm]: https://ethereum.org/en/developers/docs/evm/ [solidity]: https://www.soliditylang.org [malachite]: https://github.com/circlefin/malachite [model-based-testing]: https://en.wikipedia.org/wiki/Model-based_testing [model-checking]: https://en.wikipedia.org/wiki/Model_checking [simplex]: https://docs.rs/commonware-consensus/latest/commonware_consensus/simplex/index.html [tla]: https://lamport.azurewebsites.net/tla/tla.html [cosmos-sdk]: https://github.com/cosmos/cosmos-sdk [tendermint]: https://github.com/cometbft/cometbft [cosmwasm]: https://cosmwasm.com --- # PhD Defense Source: https://ranadeep.in/defense.md --- layout: default title: "PhD Defense" permalink: /defense --- I have the pleasure to announce that I successfully defended my Ph.D. thesis on 30 March, 2021. ## _Automated Formal Testing of Storage Systems and Applications_ The manuscript is available [here](/ranadeep_phd.pdf). The thesis jury was consisted of: - Bengt JONSSON, _Uppsala University, Sweden_ (Reviewer) - Ilya SERGEY, _Yale-NUS College, Singapore_ (Reviewer) - Mihaela SIGHIREANU, _ENS Paris-Saclay_ (Examiner) - Noam RINETZKY, _Tel Aviv University, Israel_ (Examiner) - Viktor VAFEIADIS, _Max Planck Institute for Software Systems, Kaiserslautern_ (Examiner) - Ahmed BOUAJJANI, _Université de Paris_ (Advisor) - Constantin ENEA, _Université de Paris_ (Advisor) --- _Abstract:_ > As internet grows to be cheaper and faster, distributed software systems and applications are becoming more and more ubiquitous. Today they are the backbone of a large number of online services like banking, e-commerce, social networking, etc. As the popularity of these softwares increases, it is very important that they ensure strong levels of reliability and security.

> Modern distributed software is centered around using large-scale storage systems for storing and retrieving data. To ensure persistence and availability of data in the presence of failures, these systems maintain data in multiple copies that are stored on different nodes in the network. Then, for performance reasons, these copies are allowed to (temporarily) diverge, an instance of the so-called weak-consistency, which makes the semantics of concurrent accesses to data quite complex.

> Over the recent years, many solutions for implementing weakly-consistent storage systems have been proposed. These implementations are most often very complex and error-prone. The specific levels of weak consistency they ensure are most often described only informally, which makes it difficult to reason about them. Moreover, in many cases, there are significant discrepancies between the guarantees claimed in their documentation and the guarantees that they really provide.

> The objective of this dissertation is to propose algorithmic techniques for automated testing of weakly-consistent distributed systems against formal specifications. We focus on an important class of distributed data types, called Conflict-Free Replicated Data Types (CRDTs for short), that include many variations like registers, flags, sets, arrays, etc., and on Transactional Systems (Databases), which enable computations on shared data that are isolated from other concurrent computations and resilient to failures. We introduce formal specifications for such systems and investigate the asymptotic complexity of checking whether a given execution conforms to such specifications. We also study the problem of testing applications that run on top of weakly-consistent transactional systems, introducing a mock in-memory storage system that simulates the behaviors of such systems according to their formal specifications.