I’m a compiler engineer at Efficient Computer where I am building compilers (duh!) for novel, low-power, dataflow architectures. Prior to this, I obtained my Master’s degree from Carnegie Mellon University, and spent some time there as a Research Associate at the PASTA lab. Before CMU, I worked at Microsoft Research India as a Research Fellow in the Programming Languages and Software Engineering group. I obtained my bachelor’s degree in Computer Science and Engineering from National Institute of Technology Karnataka in India.

Broadly, I am interested in program analysis, compilers and security. More specifically, my work and research aim to improve the efficiency, reliability and security of software and programs. At CMU, MSR and CertiK, I built compilers and tools that use formal methods and other automated reasoning techniques to guarantee software and system security. Currently, my work focuses on reducing the energy consumption of programs on custom hardware while maintaining programmability.

When I’m not working, I play a lot of chess. (Fun fact: I got to meet and play with Magnus Carlsen a couple of years ago!) I also like to read fiction, play the guitar and draw.

Experience

Publications

• Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM

  ArXiv, January 2025

  Ao Li, Byeongjee Kang, Vasudev Vikram, Isabella Laybourn, Samvid Dharanikota, Shrey Tiwari, Rohan Padhye

   Paper    Abstract

  Concurrency bugs are hard to discover and reproduce. Prior work has developed sophisticated algorithms to search for concurrency bugs, such as partial order sampling (POS); however, fundamental limitations with existing platforms for concurrency control hinder effective testing of real-world software. We observe that the design space for concurrency control on managed code involves complex trade-offs between expressibility, applicability, and maintainability on the one hand, and bug-finding efficiency on the other hand. This paper presents Fray, a platform for performing push-button concurrency testing of data-race-free JVM programs. The key insight behind Fray is that effective controlled concurrency testing requires orchestrating thread interleavings without replacing existing concurrency primitives, while encoding their semantics for faithfully expressing the set of all possible program behaviors. Fray incorporates a novel concurrency control mechanism called shadow locking, designed to make controlled concurrency testing practical and efficient for JVM programs. In an empirical evaluation on 53 benchmark programs with known bugs (SCTBench and JaConTeBe), Fray with random search finds 70% more bugs than JPF and 77% more bugs than RR's chaos mode. We also demonstrate Fray's push-button applicability on 2,655 tests from Apache Kafka, Lucene, and Google Guava. In these mature projects, Fray successfully discovered 18 real-world concurrency bugs that can cause 363 tests to fail reproducibly.

  
  
• Owl: Compositional Verification of Security Protocols via an Information-Flow Type System

  IEEE S&P 2023, March 2023

  Joshua Gancher, Sydney Gibson, Pratap Singh, Samvid Dharanikota, Bryan Parno

   Paper    Abstract

  Computationally sound protocol verification tools promise to deliver full-strength cryptographic proofs for security protocols. Unfortunately, current tools lack either modularity or automation. We propose a new approach based on a novel use of information flow and refinement types for sound cryptographic proofs. Our framework, Owl, allows type-based modular descriptions of security protocols, wherein disjoint subprotocols can be programmed and automatically proved secure separately. We give a formal security proof for Owl via a core language which supports standard symmetric and asymmetric primitives, Diffie-Hellman operations, and hashing via random oracles. We also implement a type checker for Owl along with a prototype extraction mechanism to Rust, and evaluate it on 14 case studies, including (simplified forms of) SSH key exchange and Kerberos.

  
  
• Celestial: A Smart Contracts Verification Framework

  FMCAD 2021, October 2021

  Samvid Dharanikota, Suvam Mukherjee, Chandrika Bhardwaj, Aseem Rastogi, Akash Lal

   Paper    Abstract

  We present Celestial, a framework for formally verifying smart contracts written in the Solidity language for the Ethereum blockchain. Celestial allows programmers to write expressive functional specifications for their contracts. It translates the contracts and the specifications to F* to formally verify, against an F* model of the blockchain semantics, that the contracts meet their specifications. Once the verification succeeds, Celestial performs an erasure of the specifications to generate Solidity code for execution on the Ethereum blockchain. We use Celestial to verify several real-world smart contracts from different application domains such as tokens, digital wallets, and governance. Our experience shows that Celestial is a valuable tool for writing high-assurance smart contracts.

  
  
• Breeding Unicorns: Developing Trustworthy and Scalable Randomness Beacons

  PLOS ONE, April 2020

  Samvid Dharanikota, Rene Rydhof Hansen, Michael Jensen, Sebastian Ro Kristensen, Matthias Sass Michno, Yvonne-Anne Pignolet, Stefan Schmid

   Paper    Abstract

  Randomness beacons are services that periodically emit a random number, allowing users to agree on the same random outcome without trusting anyone: ideally, the randomness beacon is secure (cannot be influenced) and transparent (can be monitored by users). Hence, such randomness beacons can serve as an important primitive for smart contracts in a variety of contexts. In this paper we aim to bridge the gap between theory and practice of public beacon design inspired by the unicorn protocol of Lenstra and Wesolowski using verifiable delay functions. We first present a structured security analysis, based on which we design, implement, and evaluate a trustworthy and efficient randomness beacon allowing users to join at any time. We then compare different implementation and deployment options on distributed ledgers, and report on a Ethereum smart contract-based lottery using our beacon.

  
  
• CollabChain: Blockchain-Backed Trustless Web-Based Volunteer Computing Platform

  IFIP International Conference on Computer Information Systems and Industrial Management (pp. 509-522), September 2019

  Samvid Dharanikota, Sagar Bharadwaj KS, Adarsh Honawad, K. Chandrasekaran

   Paper    Abstract

  Volunteer computing is a distributed computing model in which individuals in possession of computing resources volunteer to provide them to a project. Owing to the availability of billions of computing devices all over the world, volunteer computing can help solve problems that are larger in scale even for supercomputers. However, volunteer computing projects are difficult to launch and deploy. These platforms also force volunteers to trust the authenticity of the project owner and to blindly accept credits allotted to their contribution by the project owner. As a result, very few high-profile trusted projects are able to sustain in this system. In this paper, we present an incentivized web-based volunteer computing platform that functions as a market place to buy and sell computing power. Launching a project on the system and contributing to an existing project happens over the browser without the need for a specialized software or hardware. We introduce the application of blockchain to remove the need to trust any other party in the system. We also present a prototype implementation and solve NP-Problems as examples using the proposed prototype.

  
  
• Blockchain Research and Applications: A Systematic Mapping Study

  Springer IETE International Conference on Blockchain Technology (IC-BCT 2019), March 2019

  Samvid Dharanikota, Sagar Bharadwaj KS, Adarsh Honawad, K. Chandrasekaran

   Paper    Abstract

  Brought to the limelight by the famous Bitcoin, blockchain has since evolved, and now sees a lot of use cases apart from cryptocurrencies, such as in distributed storage systems, finance, healthcare, and so on. It is, therefore, an area of scrutiny by a lot of researchers and application developers. A significant amount of research on blockchain involves the application of blockchain technology to solve problems from various domains or improve the existing architecture of blockchain itself. The recent trend towards the decentralization of the Internet has given rise to many decentralized applications which also rely fundamentally on blockchain. In this paper, we conducted a systematic mapping study on blockchain technologies. The objective of the study is to identify and map various domains of research related to blockchain and recognize possible directions for future research. We do so by formulating a set of well-defined research questions and providing answers to them.

  
  

Projects

• Verified Datalog Engine Nov 2022 - Dec 2022
• Embedded OS Sep 2022 - Dec 2022
• CollabChain Nov 2018 - Mar 2019
• Low-rate TCP Targetted DoS Attack Simulation Jan 2018 - Apr 2018

Misc.

• Artifact reviewer for ICFP 2025
• Student volunteer for PLDI 2022
• Artifact reviewer for SAS 2021