73 Amazon Research Award recipients announced

Awardees, who represent 46 universities in 10 countries, have access to Amazon public datasets, along with AWS AI/ML services and tools.

By Amazon Research Awards team

June 3, 2025

Amazon Research Awards (ARA) provides unrestricted funds and AWS Promotional Credits to academic researchers investigating various research topics in multiple disciplines. This cycle, ARA received many excellent research proposals from across the world and today is publicly announcing 73 award recipients who represent 46 universities in 10 countries.

This announcement includes awards funded under five call for proposals during the fall 2024 cycle: AI for Information Security, Automated Reasoning, AWS AI, AWS Cryptography, and Sustainability. Proposals were reviewed for the quality of their scientific content and their potential to impact both the research community and society. Additionally, Amazon encourages the publication of research results, presentations of research at Amazon offices worldwide, and the release of related code under open-source licenses.

Recipients have access to more than 700 Amazon public datasets and can utilize AWS AI/ML services and tools through their AWS Promotional Credits. Recipients also are assigned an Amazon research contact who offers consultation and advice, along with opportunities to participate in Amazon events and training sessions.

AI for Information Security

Recipient	University	Research title
Christopher Amato	Northeastern University	Multi-Agent Reinforcement Learning Cyber Defense for Securing Cloud Computing Platforms
Bernd Bischl	Ludwig Maximilian University of Munich	Improving Generative and Foundation Models Reliability via Uncertainty-awareness
Shiqing Ma	University Of Massachusetts Amherst	LLM and Domain Adaptation for Attack Detection
Alina Oprea	Northeastern University	Multi-Agent Reinforcement Learning Cyber Defense for Securing Cloud Computing Platforms
Roberto Perdisci	University of Georgia	ContextADBench: A Comprehensive Benchmark Suite for Contextual Anomaly Detection

Automated Reasoning

Recipient	University	Research title
Nada Amin	Harvard University	LLM-Augmented Semi-Automated Proofs for Interactive Verification
Suguman Bansal	Georgia Institute of Technology	Certified Inductive Generalization in Reinforcement Learning
Ioana Boureanu	University of Surrey	Phoebe+: An Automated-Reasoning Tool for Provable Privacy in Cryptographic Systems
Omar Haider Chowdhury	Stony Brook University	Restricter: An Automatic Tool for Authoring Amazon Cedar Access Control Policies with the Principle of Least Privilege
Stefan Ciobaca	Alexandru Ioan Cuza University	An Interactive Proof Mode for Dafny
João Ferreira	INESC-ID	Polyglot Automated Program Repair for Infrastructure as Code
Sicun Gao	University Of California, San Diego	Monte Carlo Trees with Conflict Models for Proof Search
Mirco Giacobbe	University of Birmingham	Neural Software Verification
Tobias Grosser	University of Cambridge	Synthesis-based Symbolic BitVector Simplification for Lean
Ronghui Gu	Columbia University	Scaling Formal Verification of Security Properties for Unmodified System Software
Alexey Ignatiev	Monash University	Huub: Next-Gen Lazy Clause Generation
Kenneth McMillan	University of Texas At Austin	Synthesis of Auxiliary Variables and Invariants for Distributed Protocol Verification
Alexandra Mendes	University of Porto	Overcoming Barriers to the Adoption of Verification-Aware Languages
Jason Nieh	Columbia University	Scaling Formal Verification of Security Properties for Unmodified System Software
Rohan Padhye	Carnegie Mellon University	Automated Synthesis and Evaluation of Property-Based Tests
Nadia Polikarpova	University Of California, San Diego	Discovering and Proving Critical System Properties with LLMs
Fortunat Rajaona	University of Surrey	Phoebe+: An Automated-Reasoning Tool for Provable Privacy in Cryptographic Systems
Subhajit Roy	Indian Institute of Technology Kanpur	Theorem Proving Modulo LLM
Gagandeep Singh	University of Illinois At Urbana–Champaign	Trustworthy LLM Systems using Formal Contracts
Scott Stoller	Stony Brook University	Restricter: An Automatic Tool for Authoring Amazon Cedar Access Control Policies with the Principle of Least Privilege
Peter Stuckey	Monash University	Huub: Next-Gen Lazy Clause Generation
Yulei Sui	University of New South Wales	Path-Sensitive Typestate Analysis through Sparse Abstract Execution
Nikos Vasilakis	Brown University	Semantics-Driven Static Analysis for the Unix/Linux Shell
Ping Wang	Stevens Institute of Technology	Leveraging Large Language Models for Reasoning Augmented Searching on Domain-specific NoSQL Database
John Wawrzynek	University of California, Berkeley	GPU-Accelerated High-Throughput SAT Sampling

AWS AI

Recipient	University	Research title
Panagiotis Adamopoulos	Emory University	Generative AI solutions for The Spillover Effect of Fraudulent Reviews on Product Recommendations
Vikram Adve	University of Illinois at Urbana–Champaign	Fellini: Differentiable ML Compiler for Full-Graph Optimization for LLM Models
Frances Arnold	California Institute of Technology	Closed-loop Generative Machine Learning for De Novo Enzyme Discovery and Optimization
Yonatan Bisk	Carnegie Mellon University	Useful, Safe, and Robust Multiturn Interactions with LLMs
Shiyu Chang	University of California, Santa Barbara	Cut the Crap: Advancing the Efficient Communication of Multi-Agent Systems via Spatial-Temporal Topology Design and KV Cache Sharing
Yuxin Chen	University of Pennsylvania	Provable Acceleration of Diffusion Models for Modern Generative AI
Tianlong Chen	University of North Carolina at Chapel Hill	Cut the Crap: Advancing the Efficient Communication of Multi-Agent Systems via Spatial-Temporal Topology Design and KV Cache Sharing
Mingyu Ding	University of North Carolina at Chapel Hill	Aligning Long Videos and Language as Long-Horizon World Models
Nikhil Garg	Cornell University	Market Design for Responsible Multi-agent LLMs
Jessica Hullman	Northwestern University	Human-Aligned Uncertainty Quantification in High Dimensions
Christopher Jermaine	Rice University	Fast, Trusted AI Using the EINSUMMABLE Compiler
Yunzhu Li	Columbia University	Physics-Informed Foundation Models Through Embodied Interactions
Pattie Maes	Massachusetts Institute of Technology	Understanding How LLM Agents Deviate from Human Choices
Sasa Misailovic	University of Illinois at Urbana–Champaign	Fellini: Differentiable ML Compiler for Full-Graph Optimization for LLM Models
Kristina Monakhova	Cornell University	Trustworthy extreme imaging for science using interpretable uncertainty quantification
Todd Mowry	Carnegie Mellon University	Efficient LLM Serving on Trainium via Kernel Generation
Min-hwan Oh	Seoul National University	Mutually Beneficial Interplay Between Selection Fairness and Context Diversity in Contextual Bandits
Patrick Rebeschini	University of Oxford	Optimal Regularization for LLM Alignment
Jose Renau	University of California, Santa Cruz	Verification Constrained Hardware Optimization using Intelligent Design Agentic Programming
Vilma Todri	Emory University	Generative AI solutions for The Spillover Effect of Fraudulent Reviews on Product Recommendations
Aravindan Vijayaraghavan	Northwestern University	Human-Aligned Uncertainty Quantification in High Dimensions
Wei Yang	University of Texas at Dallas	Optimizing RISC-V Compilers with RISC-LLM and Syntax Parsing
Huaxiu Yao	University of North Carolina at Chapel Hill	Aligning Long Videos and Language as Long-Horizon World Models
Amy Zhang	University of Washington	Tools for Governing AI Agent Autonomy
Ruqi Zhang	Purdue University	Efficient Test-time Alignment for Large Language Models and Large Multimodal Models
Zheng Zhang	Rutgers University-New Brunswick	AlphaQC: An AI-powered Quantum Circuit Optimizer and Denoiser

AWS Cryptography

Recipient	University	Research title
Alexandra Boldyreva	Georgia Institute of Technology	Quantifying Information Leakage in Searchable Encryption Protocols
Maria Eichlseder	Graz University of Technology, Austria	SALAD – Systematic Analysis of Lightweight Ascon-based Designs
Venkatesan Guruswami	University of California, Berkeley	Obfuscation, Proof Systems, and Secure Computation: A Research Program on Cryptography at the Simons Institute for the Theory of Computing
Joseph Jaeger	Georgia Institute of Technology	Analyzing Chat Encryption for Group Messaging
Aayush Jain	Carnegie Mellon	Large Scale Multiparty Silent Preprocessing for MPC from LPN
Huijia Lin	University of Washington	Large Scale Multiparty Silent Preprocessing for MPC from LPN
Hamed Nemati	KTH Royal Institute of Technology	Trustworthy Automatic Verification of Side-Channel Countermeasures for Binary Cryptographic Programs using the HoIBA libary
Karl Palmskog	KTH Royal Institute of Technology	Trustworthy Automatic Verification of Side-Channel Countermeasures for Binary Cryptographic Programs using the HoIBA libary
Chris Peikert	University of Michigan, Ann Arbor	Practical Third-Generation FHE and Bootstrapping
Dimitrios Skarlatos	Carnegie Mellon University	Scale-Out FHE LLMs on GPUs
Vinod Vaikuntanathan	Massachusetts Institute of Technology	Can Quantum Computers (Really) Factor?
Daniel Wichs	Northeastern University	Obfuscation, Proof Systems, and Secure Computation: A Research Program on Cryptography at the Simons Institute for the Theory of Computing
David Wu	University Of Texas At Austin	Fast Private Information Retrieval and More using Homomorphic Encryption

Sustainability

Recipient	University	Research title
Meeyoung Cha	Max Planck Institute	Forest-Blossom (Flossom): A New Framework for Sustaining Forest Biodiversity Through Outcome-Driven Remote Sensing Monitoring
Jingrui He	University of Illinois at Urbana–Champaign	Foundation Model Enabled Earth’s Ecosystem Monitoring
Pedro Lopes	University of Chicago	AI-powered Tools that Enable Engineers to Make & Re-make Sustainable Hardware
Cheng Yaw Low	Max Planck Institute	Forest-Blossom (Flossom): A New Framework for Sustaining Forest Biodiversity Through Outcome-Driven Remote Sensing Monitoring

About the Author

Amazon Research Awards team