Chandrakana Nandi

I am the Director of US R&D at Certora and affiliate assistant professor at University of Washington, Seattle. Before this, I graduated with a PhD from the PLSE group at the University of Washington, Seattle where I worked with my incredible advisors, Zachary Tatlock and Dan Grossman.

Research

I am interested in building tools for scaling automated formal verification to real-world programs; we are focusing on DeFi applications specifically. As part of this vision, we are working on new verification tools for languages like WASM and techniques to help users write formal specifications more easily using mutation testing.

I also work on equality saturation and its applications in synthesis, verification, and optimization. Our work on Carpentry Compiler and Szalinski are some of the first tools that use equality saturation as a technique for optimizing unconventional compilers and for program synthesis. We also built Ruler, a very cool tool that uses equality saturation to synthesize rewrite rules for equality saturation!

I have developed programming languages, correct compilers, and synthesis tools for computational geometry and fabrication. I still work on these topics whenever I can.

We built LambdaCAD, a functional programming language for 3D modeling that supports 3D primitives, affine operations, and boolean operators to compose designs. The LambdaCAD compiler generates a triangle mesh from a LambdaCAD program. Using our compiler infrastructure and 3D geometry kernel, we built a decompiler, called Reincarnate, that uses evaluation context to synthesize LambdaCAD programs back from meshes. Check out my thesis for more details on the correctness of our compiler for a subset of LambdaCAD and for open problems in computational fabrication that can be tackled with PL techniques! Check out our tools, papers, talks, and more.

Conference and Journal Publications

OOPSLA 2024 Practical Verification Of Smart Contracts Using Memory Splitting
Shelly Grossman, Alexander Bakst, Sameer Arora, John Toman, Mooly Sagiv, Chandrakana Nandi
pdf
ICST 2024 Using Mutation Testing To Improve and Minimize Test Suites for Smart Contracts (Industry Track)
Enzo Nicourt, Ben Kushigian, Chandrakana Nandi, Ylies Falcone
pdf
OOPSLA 2023 Equality Saturation Theory Exploration à la Carte.
Anjali Pal, Brett Saiki, Cynthia Richey, Amy Zhu, Ryan Tjoa, Oliver Flatt, Max Willsey, Zachary Tatlock, Chandrakana Nandi
pdf
POPL 2023 babble: Learning Better Abstractions with E-Graphs and Anti-Unification.
David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, Nadia Polikarpova
pdf
ACM TOG, 2022 Co-Optimization of Design and Fabrication Plans for Carpentry.
Haisen Zhao, Max Willsey, Amy Zhu, Chandrakana Nandi, Zachary Tatlock, Justin Solomon, Adriana Schulz
pdf
SFF 2021 A Roadmap Towards Parallel Printing for Desktop 3D Printers.
Molly Carton, Chandrakana Nandi, Adam Anderson, Haisen Zhao, Eva Darulova, Dan Grossman, Jeff Lipton, Adriana Schulz, Zachary Tatlock
pdf
OOPSLA 2021 Rewrite Rule Inference Using Equality Saturation.
Chandrakana Nandi, Max Willsey, Amy Zhu, Brett Saiki, Remy Wang, Adam Anderson, Adriana Schulz, Dan Grossman, Zachary Tatlock.
Distinguished Paper Award
pdf slides talk code
UIST 2021 Taxon: a Language for Formal Reasoning with Digital Fabrication Machines.
Jasper Tran O'Leary, Chandrakana Nandi, Khang Lee, Nadya Peek.
pdf
ARITH 2021 Combining Precision Tuning and Rewriting.
Brett Saiki, Oliver Flatt, Chandrakana Nandi, Zachary Tatlock, Pavel Panchekha.
pdf website
POPL 2021 Fast and Extensible Equality Saturation.
Max Willsey, Chandrakana Nandi, Remy Wang, Oliver Flatt, Pavel Panchekha, Zachary Tatlock.
Distinguished Paper Award
pdf github website
PLDI 2020 Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations.
Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman, Zachary Tatlock.
pdf github website
SIGGRAPH ASIA 2019
Carpentry Compiler.
Chenming Wu, Haisen Zhao, Chandrakana Nandi, Jeff Lipton, Zachary Tatlock, Adriana Schulz.
pdf website UW news Daily of UW Tech Crunch
ICFP 2018 Functional Programming for Compiling and Decompiling Computer-Aided Design.
Chandrakana Nandi, James R. Wilcox, Pavel Panchekha, Taylor Blau, Dan Grossman, Zachary Tatlock.
pdf github website
SNAPL 2017 Programming Language Tools and Techniques for 3D Printing.
Chandrakana Nandi, Anat Caspi, Dan Grossman, Zachary Tatlock.
pdf website
CBSE 2015 Stochastic Contracts for Runtime Checking of Component-based Real-time Systems.
Chandrakana Nandi, Aurelien Monot, Manuel Oriol.
pdf

Workshops, Theses, and Other Publications

WOSET 2024 Scaling Program Synthesis Based Technology Mapping with Equality Saturation.
Gus Henry Smith, Colin Knizek, Daniel Petrisko, Zachary Tatlock, Jonathan Balkind, Gilbert Louis Bernstein, Haobin Ni, Chandrakana Nandi.
pdf
SCF Demo 2024 Demonstrating FEDT: Supporting Characterization Experiments in Fabrication Research
Valkyrie Savage, Nóra Püsök, Harrison Goldstein, Chandrakana Nandi, Jia Yi Ren, Lora Oehlberg
pdf
LATTE 2024 There and Back Again: A Netlist's Tale with Much Egraphin'
Gus Henry Smith, Zachary D. Sisco, Thanawat Techaumnuaiwit, Jingtao Xia, Vishal Canumalla, Andrew Cheung, Zachary Tatlock, Chandrakana Nandi, Jonathan Balkind
pdf
PhD thesis, August 2021 Programming Language Tools and Techniques for Computational Fabrication.
Chandrakana Nandi.
pdf
MAPL 2017 Debugging Probabilistic Programs.
Chandrakana Nandi, Dan Grossman, Adrian Sampson, Todd Mytkowicz, Kathryn S. McKinley.
pdf
PPS 2017 Debugging Probabilistic Programs.
Chandrakana Nandi, Dan Grossman, Adrian Sampson, Todd Mytkowicz, Kathryn S. McKinley.
PLAS 2016 Automatic Trigger Generation for Rule-based Smart Homes.
Chandrakana Nandi, Michael D. Ernst.
pdf
FSE SRC 2016 Automatic Trigger Generation for End User Written Rules for Home Automation.
Chandrakana Nandi.
pdf
POPL SRC 2016 Correctness and Security for Home Automation.
Chandrakana Nandi.
poster pdf
MS thesis, August 2014 Contracts for Real-Time, Safety Critical Systems.
Chandrakana Nandi.
pdf
BS thesis, April 2012 Social Network based Analysis of Behavior.
Chandrakana Nandi.
pdf

Fun stuff

We have a fantastic running club as part of which we run all over Seattle. We also take part in numerous marathons, half-marathons and relay races!

My mom has a cool recipe blog that I help maintain. Feel free to check it out. She regularly adds delicious recipes!

Contact

The best way to reach me is by email: chandra@certora.com . You can find more details about my work in my CV.