6 citations · 15 across the 13 of their papers we have counts for
14 papers
Learning Affordances at Inference-Time for Vision-Language-Action Models
Ameesh Shah, William Chen, Adwait Godbole +3
Solving complex real-world control tasks often takes multiple tries: if we fail at first, we reflect on what went wrong, and change our strategy accordingly to avoid making the sam…
PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
Pei-Wei Chen, Shaokai Lin, Adwait Godbole +4
Several software systems are polyglot; that is, they comprise programs implemented in a combination of programming languages. Verifiers that directly run on mainstream programming…
Syzygy: Dual Code-Test C to (safe) Rust Translation using LLMs and Dynamic Analysis
Manish Shetty, Naman Jain, Adwait Godbole +2
Despite extensive usage in high-performance, low-level systems programming applications, C is susceptible to vulnerabilities due to manual memory management and unsafe pointer oper…
SemPat: Using Hyperproperty-based Semantic Analysis to Generate Microarchitectural Attack Patterns
Adwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia
Microarchitectural security verification of software has seen the emergence of two broad classes of approaches. The first is based on semantic security properties (e.g., non-interf…
Unified Fairness for Weak Memory Verification
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole +2
We consider the verification of omega-regular linear temporal properties of concurrent programs running under weak memory semantics. We observe that in particular, these properties…
Parameterized Verification under TSO with Data Types
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Florian Furbach +4
We consider parameterized verification of systems executing according to the total store ordering (TSO) semantics. The processes manipulate abstract data types over potentially inf…
Automated Conversion of Axiomatic to Operational Models: Theory and Practice
Adwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia
A system may be modelled as an operational model (which has explicit notions of state and transitions between states) or an axiomatic model (which is specified entirely as a set of…
UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu +6
UCLID5 is a tool for the multi-modal formal modeling, verification, and synthesis of systems. It enables one to tackle verification problems for heterogeneous systems such as combi…
Probabilistic Total Store Ordering
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Raj Aryan Agarwal +2
We present -- a probabilistic extension of the classical TSO semantics. For a given (finite-state) program, the operational sem…
Safety Verification of Parameterized Systems under Release-Acquire
Adwait Godbole, Shankara Narayanan Krishna, Roland Meyer
We study the safety verification problem for parameterized systems under the release-acquire (RA) semantics. It has been shown that the problem is intractable for systems with unli…
The Decidability of Verification under Promising 2.0
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole +2
In PLDI'20, Lee et al. introduced the \emph{promising } semantics PS 2.0 of the C++ concurrency that captures most of the common program transformations while satisfying the DRF gu…
Containment of Simple Regular Path Queries
Diego Figueira, Adwait Godbole, S. Krishna +3
Testing containment of queries is a fundamental reasoning task in knowledge representation. We study here the containment problem for Conjunctive Regular Path Queries (CRPQs), a na…
Controlling a population
Nathalie Bertrand, Miheer Dewaskar, Blaise Genest +2
We introduce a new setting where a population of agents, each modelled by a finite-state system, are controlled uniformly: the controller applies the same action to every agent. Th…
Controlling a Population
Nathalie Bertrand, Miheer Dewaskar, Blaise Genest +1
We introduce a new setting where a population of agents, each modelled by a finite-state system, are controlled uniformly: the controller applies the same action to every agent. Th…