publications | Dhruv C. Makwana

2026

On the Theory and Engineering of Verifying Systems C

Dhruv C. Makwana

University of Cambridge, 2026

Abs Bib PDF Website

In this thesis, I will 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 = {On the Theory and Engineering of Verifying Systems C}, url = {https://github.com/dc-mak/PhD-Thesis/releases/tag/latest}, school = {University of Cambridge}, author = {Makwana, Dhruv C.}, year = {2026}, }

2025

Fulminate: Testing CN Separation-Logic Specifications in C

Rini Banerjee, Kayvan Memarian, Dhruv Makwana, and 3 more authors

Proc. ACM Program. Lang., Jan 2025

Abs DOI Bib Video Code

Separation logic has become an important tool for formally capturing and reasoning about the ownership patterns of imperative programs, originally for paper proof, and now the foundation for industrial static analyses and multiple proof tools. However, there has been very little work on program testing of separation-logic specifications in concrete execution. At first sight, separation-logic formulas are hard to evaluate in reasonable time, with their implicit quantification over heap splittings, and other explicit existentials. In this paper we observe that a restricted fragment of separation logic, adopted in the CN proof tool to enable predictable proof automation, also has a natural and readable computational interpretation, that makes it practically usable in runtime testing. We discuss various design issues and develop this as a C+CN source to C source translation, Fulminate. This adds checks – including ownership checks and ownership transfer – for C code annotated with CN pre- and post-conditions; we demonstrate this on nontrivial examples, including the allocator from a production hypervisor. We formalise our runtime ownership testing scheme, showing (and proving) how its reified ghost state correctly captures ownership passing, in a semantics for a small C-like language.
@article{banerjee2025fulminate, author = {Banerjee, Rini and Memarian, Kayvan and Makwana, Dhruv and Pulte, Christopher and Krishnaswami, Neel and Sewell, Peter}, title = {Fulminate: Testing CN Separation-Logic Specifications in C}, year = {2025}, issue_date = {January 2025}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, volume = {9}, number = {POPL}, url = {https://doi.org/10.1145/3704879}, doi = {10.1145/3704879}, journal = {Proc. ACM Program. Lang.}, month = jan, articleno = {43}, numpages = {33}, keywords = {Android, C, pKVM, refinement types, runtime testing, separation logic, verification}, }

2023

CN: Verifying Systems C Code with Separation-Logic Refinement Types

Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, and 3 more authors

Proc. ACM Program. Lang., Jan 2023

Abs DOI Bib Video Code Website

Despite significant progress in the verification of hypervisors, operating systems, and compilers, and in verification tooling, there exists a wide gap between the approaches used in verification projects and conventional development of systems software. We see two main challenges in bringing these closer together: verification handling the complexity of code and semantics of conventional systems software, and verification usability. We describe an experiment in verification tool design aimed at addressing some aspects of both: we design and implement CN, a separation-logic refinement type system for C systems software, aimed at predictable proof automation, based on a realistic semantics of ISO C. CN reduces refinement typing to decidable propositional logic reasoning, uses first-class resources to support pointer aliasing and pointer arithmetic, features resource inference for iterated separating conjunction, and uses a novel syntactic restriction of ghost variables in specifications to guarantee their successful inference. We implement CN and formalise key aspects of the type system, including a soundness proof of type checking. To demonstrate the usability of CN we use it to verify a substantial component of Google’s pKVM hypervisor for Android.
@article{pulte2023cn, author = {Pulte, Christopher and Makwana, Dhruv C. and Sewell, Thomas and Memarian, Kayvan and Sewell, Peter and Krishnaswami, Neel}, title = {CN: Verifying Systems C Code with Separation-Logic Refinement Types}, year = {2023}, issue_date = {January 2023}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, volume = {7}, number = {POPL}, url = {https://doi.org/10.1145/3571194}, doi = {10.1145/3571194}, journal = {Proc. ACM Program. Lang.}, month = jan, articleno = {1}, numpages = {32}, keywords = {Android, C, pKVM, refinement types, separation logic, verification}, }

2019

NumLin: Linear Types for Linear Algebra

Dhruv C. Makwana and Neelakantan R. Krishnaswami

In 33rd European Conference on Object-Oriented Programming (ECOOP 2019), Jan 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},
}

2018

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}, }