Publications Adwait Godbole

* denotes undergraduate research mentee, † denotes equal contribution

Syzygy: Dual Code-Test C to (safe) Rust Translation
using LLMs and Dynamic Analysis

SemPat: From Hyperproperties to Attack Patterns for
Scalable Microarchitectural Security Analysis

Lifting Micro-Update Models from RTL for Formal Security Analysis

PipeSynth: Automated Synthesis of
Microarchitectural Axioms for Memory Consistency

Towards A Formally Verified Fully Homomorphic Encryption Compute Engine*

J. Casas, Z. Yang, W. Wang, A. Godbole and J. Yang

Overcoming Memory Weakness with Unified Fairness:
Systematic Verification of Liveness in Weak Memory Models

Parameterized Verification under TSO with Data Types

P. A. Abdulla, M. F. Atig, F. Furbach,
A. Godbole, Y. G. Hendi, S. N. Krishna and S. Spengler

Automated conversion of axiomatic to
operational models: Theory and practice

Parameterized Verification under Release Acquire is PSPACE-complete

Probabilistic Total Store Ordering

The Decidability of Verification under PS 2.0

Containment of Simple Conjunctive Regular Path Queries

D. Figueira, A. Godbole, S. Krishna, W. Martens, M. Niewerth and T. Trautner

Modelling and Verifying Security Oriented Resource Partioning Schemes

UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis