Aditya V. Thakur

Aditya V. Thakur is an Associate Professor of Computer Science and Vice Chair of the Graduate Group in Computer Science (GGCS) at the University of California, Davis College of Engineering. His research spans programming languages, machine learning, formal methods, and software engineering with a focus on developing tools and techniques for correct software development.

Thakur's research interests primarily focus on programming languages, machine learning, formal methods, and software engineering. His work specifically targets the analysis and repair of deep neural networks, neuro-symbolic program analysis, and static program analysis. He leads the Davis Automated Reasoning Group (DARG), which develops theoretical formalisms and practical tools to tackle software challenges across various systems from IoT firmware to deep neural networks with billions of parameters.

His recent publications demonstrate a strong focus on applying formal methods to machine learning systems and traditional software verification. The trend shows increasing integration of neural networks with formal verification techniques, particularly in safety-critical applications. His work on provable repair of deep neural networks has gained significant traction in top conferences like PLDI and NeurIPS.

• DOE Early Career award (2021)
• NSF CAREER award (2021)
• Facebook Probability and Programming Research Award (2019, 2020)
• Facebook Testing and Verification (TAV) Research Award (2018)
• DECOR 2018 Research Award

Thakur has advised several notable students including Matthew Sotoudeh (who received NSF GRFP and Chancellor's Award), Sung Kook Kim (who received Radhia Cousot Young Researcher Best Paper Award), and Daniel DeFreez (who won ESEC/FSE Student Research Competition). His research has received substantial funding from NSF, DOE, and industry partners including Facebook and Microsoft. His parallel fixpoint algorithm has been integrated into NASA IKOS and Facebook SPARTA, and his verified DICE implementation has been deployed on Microsoft Azure.

Thakur leads the Davis Automated Reasoning Group (DARG), which develops tools like PRDNN (Provable Repair of Deep Neural Networks), SyReNN (Symbolic Representation of Neural Networks), PIKOS (Parallel Abstract Interpreter), and MIKOS (Memory-Efficient Abstract Interpreter. His group's neuro-symbolic program analysis tools have found over 200 bugs in critical open-source projects including the Linux kernel, OpenSSL, mbedTLS, Pidgin, and netdata.