Dr. Aalok Thakkar

Research Scientist focussed on integrating formal methods and artificial intelligence.

Seattle, Washington, United States of America

Research Expertise

programming languages

verification

logic

synthesis

Computer Science Applications

Health Informatics

Health Information Management

Safety, Risk, Reliability and Quality

Software

About

My research focuses on integrating **formal methods** and **artificial intelligence**. In particular, I have worked on applying formal methods in the context of programming-by-examples (PBE) for relational queries, synthesis of reactive programs, bounded model checking, and verification of smart contracts. Currently, I work with Movement Labs on designing the Fractal interpreter will allow users to deploy Solidity smart contracts directly on Movement's M1 blockchain. Previously, I have worked with Aptos Labs, Amazon AWS, Nokia Bell Labs, and Adobe India.

Publications

Concurrency in Boolean networks

Natural Computing / Jun 08, 2019

Chatain, T., Haar, S., Kolčák, J., Paulevé, L., & Thakkar, A. (2019). Concurrency in Boolean networks. Natural Computing, 19(1), 91–109. https://doi.org/10.1007/s11047-019-09748-4

Example-guided synthesis of relational queries

Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation / Jun 18, 2021

Thakkar, A., Naik, A., Sands, N., Alur, R., Naik, M., & Raghothaman, M. (2021, June 18). Example-guided synthesis of relational queries. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. https://doi.org/10.1145/3453483.3454098

Reopening businesses and risk of COVID-19 transmission

npj Digital Medicine / Mar 16, 2021

O’Donoghue, A., Dechen, T., Pavlova, W., Boals, M., Moussa, G., Madan, M., Thakkar, A., DeFalco, F. J., & Stevens, J. P. (2021). Reopening businesses and risk of COVID-19 transmission. Npj Digital Medicine, 4(1). https://doi.org/10.1038/s41746-021-00420-9

Early and Systematic Validation of Formal Models

Formal Methods and Software Engineering / Jan 01, 2023

Stock, S. (2023). Early and Systematic Validation of Formal Models. In Lecture Notes in Computer Science (pp. 255–260). Springer Nature Singapore. https://doi.org/10.1007/978-981-99-7584-6_16

ArXiv preprint server plans multimillion-dollar overhaul

Nature / Jun 29, 2016

Van Noorden, R. (2016). ArXiv preprint server plans multimillion-dollar overhaul. Nature, 534(7609), 602–602. https://doi.org/10.1038/534602a

Infinitude of Primes Using Formal Languages

The American Mathematical Monthly / Sep 14, 2018

Thakkar, A. (2018). Infinitude of Primes Using Formal Languages. The American Mathematical Monthly, 125(8), 745–749. https://doi.org/10.1080/00029890.2018.1496761

Mobius: Synthesizing Relational Queries with Recursive and Invented Predicates

Proceedings of the ACM on Programming Languages / Oct 16, 2023

Thakkar, A., Sands, N., Petrou, G., Alur, R., Naik, M., & Raghothaman, M. (2023). Mobius: Synthesizing Relational Queries with Recursive and Invented Predicates. Proceedings of the ACM on Programming Languages, 7(OOPSLA2), 1394–1417. https://doi.org/10.1145/3622847

Relational Query Synthesis ⋈ Decision Tree Learning

Proceedings of the VLDB Endowment / Oct 01, 2023

Naik, A., Thakkar, A., Stein, A., Alur, R., & Naik, M. (2023). Relational Query Synthesis ⋈ Decision Tree Learning. Proceedings of the VLDB Endowment, 17(2), 250–263. https://doi.org/10.14778/3626292.3626306

Reopening Businesses and Risk of COVID-19 Transmission

May 25, 2020

O’Donoghue, A., Dechen, T., Pavlova, W., Boals, M., Moussa, G., Madan, M., Thakkar, A., DeFalco, F. J., & Stevens, J. P. (2020). Reopening Businesses and Risk of COVID-19 Transmission. https://doi.org/10.1101/2020.05.24.20112110

Synthesis of coordination programs from linear temporal specifications

Proceedings of the ACM on Programming Languages / Dec 20, 2019

Bansal, S., Namjoshi, K. S., & Sa’ar, Y. (2019). Synthesis of coordination programs from linear temporal specifications. Proceedings of the ACM on Programming Languages, 4(POPL), 1–27. https://doi.org/10.1145/3371122

On the Completeness of Compositional Reasoning

Computer Aided Verification / Jan 01, 2000

Namjoshi, K. S., & Trefler, R. J. (2000). On the Completeness of Compositional Reasoning. In Lecture Notes in Computer Science (pp. 139–153). Springer Berlin Heidelberg. https://doi.org/10.1007/10722167_14

On the Use of Rewriting Logic for Verification of Distributed Software Architecture Description Based LfP

16th IEEE International Workshop on Rapid System Prototyping (RSP'05)

Jerad, C., & Barkaoui, K. (n.d.). On the Use of Rewriting Logic for Verification of Distributed Software Architecture Description Based LfP. 16th IEEE International Workshop on Rapid System Prototyping (RSP’05). https://doi.org/10.1109/rsp.2005.34

Education

Chennai Mathematical Institute

Bachelor's of Science, Mathematics

Siruseri

University of Pennsylvania

Ph.D., Computer and Information Science / May, 2023

Philadelphia, Pennsylvania, United States of America

Experience

Movement Labs

Research Engineer / February, 2024 — Present

Aptos Labs

Research Scientist / July, 2023 — January, 2024

Join Aalok on NotedSource!

Join Now

At NotedSource, we believe that professors, post-docs, scientists and other researchers have deep, untapped knowledge and expertise that can be leveraged to drive innovation within companies. NotedSource is committed to bridging the gap between academia and industry by providing a platform for collaboration with industry and networking with other researchers.

For industry, NotedSource identifies the right academic experts in 24 hours to help organizations build and grow. With a platform of thousands of knowledgeable PhDs, scientists, and industry experts, NotedSource makes connecting and collaborating easy.

For academic researchers such as professors, post-docs, and Ph.D.s, NotedSource provides tools to discover and connect to your colleagues with messaging and news feeds, in addition to the opportunity to be paid for your collaboration with vetted partners.