Publications Adwait Godbole

* denotes undergraduate research mentee

SemPat: Using Hyperproperty-based Semantic Analysis
to Generate Microarchitectural Attack Patterns

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