Description

Amazon Research Awards supports research applying mathematical logic to answer questions and prove properties of critical computer systems. The call aims to improve security, availability, and robustness in the cloud through analysis of policies and configurations, verification of protocols and programs, and analysis of generative AI output. These approaches support AWS services and customer-visible features.

Research priorities include sound neurosymbolic reasoning combining large language models, automated solving, and proof checking; interfaces with theorem provers; and symbolic approaches to formalizing system specifications. The call also welcomes advances in solvers, static analysis, software model checking, correct-by-construction methods, synthesis, distributed-system verification, privacy, cryptography, hardware modeling, complementary testing, and perception-network robustness. Selection emphasizes relevance to Amazon problems, research impact, and a larger, more diverse automated reasoning community.