aalok thakkar.

I am a research engineer at Movement Labs, where I work on the Fractal project. Fractal is an interpreter for Solidity smart contracts that enables their deployment on M1, a Move-based chain.

In general, my research focuses on integrating formal methods and artificial intelligence. 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. In 2023, I obtained my Ph.D. advised by Rajeev Alur and Mayur Naik. During this time, I developed the example-guided framework for synthesis of relational queries.

In the past, I have worked with Aptos Labs, AWS Automated Reasoning Group, Nokia Bell Labs, Adobe Systems, and Laboratoire Specification et Verification. .

news:

Feb 2024: I have joined Movement Labs as a reasearch engineer.