Controlling a population. - Nathalie Bertrand 001; Miheer Dewaskar; Blaise Genest; Hugo Gimbert; Adwait Amit Godbole (Log. Methods Comput. Sci., 2019)

Containment of Simple Conjunctive Regular Path Queries. - Diego Figueira; Adwait Godbole; S. Krishna 004; Wim Martens; Matthias Niewerth; Tina Trautner (KR, 2020)

Containment of Simple Regular Path Queries. - Diego Figueira; Adwait Godbole; S. Krishna 004; Wim Martens; Matthias Niewerth; Tina Trautner (CoRR, 2020)

The Decidability of Verification under Promising 2.0. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Adwait Godbole; Shankaranarayanan Krishna; Viktor Vafeiadis (CoRR, 2020)

The Decidability of Verification under PS 2.0. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Adwait Godbole; S. Krishna 004; Viktor Vafeiadis (ESOP, 2021)

Safety Verification of Parameterized Systems under Release-Acquire. - Adwait Godbole; Shankara Narayanan Krishna; Roland Meyer 001 (CoRR, 2021)

UCLID5: Multi-modal Formal Modeling, Verification, and Synthesis. - Elizabeth Polgreen; Kevin Cheang; Pranav Gaddamadugu; Adwait Godbole; Kevin Laeufer; Shaokai Lin; Yatin A. Manerkar; Federico Mora 002; Sanjit A. Seshia (CAV (1), 2022)

Probabilistic Total Store Ordering. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Raj Aryan Agarwal; Adwait Godbole; S. Krishna 004 (ESOP, 2022)

Automated Conversion of Axiomatic to Operational Models: Theory and Practice. - Adwait Godbole; Yatin A. Manerkar; Sanjit A. Seshia (FMCAD, 2022)

Parameterized Verification under Release Acquire is PSPACE-complete. - Shankaranarayanan Krishna; Adwait Godbole; Roland Meyer 001; Soham Chakraborty 001 (PODC, 2022)

PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory Consistency. - Chase Norman; Adwait Godbole; Yatin A. Manerkar (ASPLOS (3), 2023)

Overcoming Memory Weakness with Unified Fairness - Systematic Verification of Liveness in Weak Memory Models. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Adwait Godbole; Shankaranarayanan Krishna; Mihir Vahanwala (CAV (1), 2023)

Towards A Formally Verified Fully Homomorphic Encryption Compute Engine. - Jeremy Casas; Zhenkun Yang; Wen Wang; Jin Yang 006; Adwait Godbole (DAC, 2023)

Modelling and Verification of Security-Oriented Resource Partitioning Schemes. - Adwait Godbole; Leiqi Ye; Yatin A. Manerkar; Sanjit A. Seshia (FMCAD, 2023)

Parameterized Verification under TSO with Data Types. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Florian Furbach; Adwait Amit Godbole; Yacoub G. Hendi; Shankara Narayanan Krishna; Stephan Spengler (TACAS (1), 2023)

Overcoming Memory Weakness with Unified Fairness. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Adwait Godbole; Shankaranarayanan Krishna; Mihir Vahanwala (CoRR, 2023)

Lifting Micro-Update Models from RTL for Formal Security Analysis. - Adwait Godbole; Kevin Cheang; Yatin A. Manerkar; Sanjit A. Seshia (ASPLOS (2), 2024)

Fairness and Liveness Under Weak Consistency. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Adwait Godbole; Shankara Narayanan Krishna; Mihir Vahanwala (Taming the Infinities of Concurrency, 2024)

SemPat: From Hyperproperties to Attack Patterns for Scalable Analysis of Microarchitectural Security. - Adwait Godbole; Yatin A. Manerkar; Sanjit A. Seshia (CCS, 2024)

SemPat: Using Hyperproperty-based Semantic Analysis to Generate Microarchitectural Attack Patterns. - Adwait Godbole; Yatin A. Manerkar; Sanjit A. Seshia (CoRR, 2024)

Syzygy: Dual Code-Test C to (safe) Rust Translation using LLMs and Dynamic Analysis. - Manish Shetty; Naman Jain; Adwait Godbole; Sanjit A. Seshia; Koushik Sen (CoRR, 2024)

$ mathbf{{ textsc {PyCaliper}}}$: Python-Embedded Infrastructure for RTL Verification and Specification Synthesis. - Adwait Godbole; Brian Huffman; Fangfei Liu; Carlos V. Rozas; Sanjit A. Seshia (CAV (3), 2025)

PolyVer: A Compositional Approach for Polyglot System Modeling and Verification. - Pei-Wei Chen; Shaokai Lin; Adwait Godbole; Ramneet Singh; Elizabeth Polgreen; Edward A. Lee; Sanjit A. Seshia (CoRR, 2025)