publications | Dhruv Makwana

2026

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

Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows

Zain K Aamer, Rini Banerjee, Hiroyuki Katsura, and 8 more authors

Proc. ACM Program. Lang., Jun 2026

We seek to enable more flexible use of rich specifications in a variety of ways that smoothly extend conventional software development practice. We show how a single specification language, based on separation logic to capture the subtle ownership disciplines of systems code, can be used for runtime assertion checking, for property-based testing, and for formal machine-checked proof—and how each of these complements and supports the others. We demonstrate all this on a challenging example: a component of a production hypervisor, running both stand-alone at user level and in situ in the hypervisor.

@article{aamer2026code,
  author = {Aamer, Zain K and Banerjee, Rini and Katsura, Hiroyuki and Kaloper-Mer{\v s}injak, David and Economou, Dimitrios J. and Memarian, Kayvan and Makwana, Dhruv and Krishnaswami, Neel and Pierce, Benjamin C. and Pulte, Christopher and Sewell, Peter},
  title = {Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows},
  year = {2026},
  issue_date = {June 2026},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {10},
  number = {PLDI},
  url = {https://doi.org/10.1145/3808278},
  doi = {10.1145/3808278},
  journal = {Proc. ACM Program. Lang.},
  month = jun,
  articleno = {200},
  numpages = {27},
  keywords = {C, specification, runtime testing, property-based testing, refinement types, verification, pKVM, Android},
}

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

2017

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