Dhruv C. 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 the CN C verification tool, 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{makwana2026theory, 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}, }