Dhruv Makwana

Based in London, UK

I work as a Researcher at Math, Inc. We are hiring researchers with experience in software verification - please apply!

I am in the process of submitting my PhD thesis at the University of Cambridge, on CN, a verification tool for C, supervised by Neel Krishnaswami and Peter Sewell.

A general theme of my work has been the intersection of elegant abstractions, technical infrastructure problems and readable, working code. So far, I have focused on tooling performance, types, and verification. I’m enthusiastic about supporting others: I’ve trained new hires and mentored interns, given talks, made educational videos, and taught undergrads and children.

On the personal side of things, I am a practising Buddhist, under the tutelage of Beth Upton. I enjoy long meditation retreats, volunteer with local animal rights groups and enjoy cooking (specializing in vegan Gujarati cuisine). Some very kind friends gave me a wonderful gift a while back: they listened to me speaking about my life and my views, and recorded it for posterity.

Jamie Woodhouse’s Sentientism Podcast, and show notes.
Coffee’s on Me, David Quan, with a 1-minute summary.

selected publications

CN: Theory and Engineering of Verifying C

Dhruv C. Makwana

University of Cambridge, 2026

Abs Bib PDF Website

In this thesis, I argue that building a verification tool for C, suitable for handling low-level systems programming idioms, is two parts engineering, and one part theory. Little of the theory is novel or complex, but its application at scale presents new challenges and insights.
@phdthesis{makwana2026cn, title = {CN: Theory and Engineering of Verifying C}, url = {https://github.com/dc-mak/PhD-Thesis/releases/tag/latest}, school = {University of Cambridge}, author = {Makwana, Dhruv C.}, year = {2026}, }

NumLin: Linear Types for Linear Algebra

Dhruv C. Makwana and Neelakantan R. Krishnaswami

In 33rd European Conference on Object-Oriented Programming (ECOOP 2019), 2019

DOI Bib Video Code

@inproceedings{makwana2019numlin,
  author = {Makwana, Dhruv C. and Krishnaswami, Neelakantan R.},
  title = {{NumLin: Linear Types for Linear Algebra}},
  booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages = {14:1--14:25},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  isbn = {978-3-95977-111-5},
  issn = {1868-8969},
  year = {2019},
  volume = {134},
  editor = {Donaldson, Alastair F.},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address = {Dagstuhl, Germany},
  url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.14},
  urn = {urn:nbn:de:0030-drops-108069},
  doi = {10.4230/LIPIcs.ECOOP.2019.14},
  annote = {Keywords: numerical, linear, algebra, types, permissions, OCaml},
}

Implementing Balanced Polling for OCaml

Dhruv C. Makwana

Mar 2018

Abs Bib PDF Code Website

Native OCaml compilation does not guarantee the existence of safepoints on all execution paths. This means valid programs can crash or experience delayed thread communication. I fix this by inserting safepoints during code generation following Feeley’s algorithm. As a result, more OCaml programs can run natively and there now exists an upper bound on thread communication latency for multi-core OCaml. However, this comes with a potential increase in their execution times.
@misc{makwana2018safepoints, type = {Report}, author = {Makwana, Dhruv C.}, month = mar, year = {2018}, title = {Implementing Balanced Polling for OCaml}, url = {https://github.com/ocaml/ocaml/files/4148541/mcd-report.pdf}, }
Exploring the structure of mathematical theories using graph databases

Dhruv C. Makwana

Part II Dissertation, Computer Science Tripos, University of Cambridge , May 2017

Abs Bib PDF Code

In this dissertation, I describe a new tool I implemented for Coq users that aimed to (a) represent Coq libraries as Neo4j (graph) databases and (b) provide a library of queries with the goal of highlighting the structure of and relationship between proof-objects. It achieves (b) by using network-analysis techniques usually associated with social-networks. I give examples of new questions that can now be answered by querying the library and show how network-analysis algorithms and visualisations can provide new insights into the structure of a Coq library. Its feature set, performance and output on real-world Coq libraries show that this project has potential to be useful to the Coq community.
@misc{makwana2017coqgraphs, type = {Dissertation}, author = {Makwana, Dhruv C.}, month = may, year = {2017}, title = {Exploring the structure of mathematical theories using graph databases}, howpublished = {Part II Dissertation, Computer Science Tripos, University of Cambridge}, keywords = {Coq, proof assistant, graph databases, Neo4j, network analysis, Odd Order Theorem}, }