In July 2021, Amazon notified applicants that they were recipients of the Spring 2021 Amazon Research Awards, a program that provides unrestricted funds and AWS Promotional Credits to academic researchers investigating research topics across a number of disciplines.
Today, we’re publicly announcing the 26 award recipients who represent 25 universities in 11 countries. Each award is intended to support the work of one to two graduate students or postdoctoral students for one year, under the supervision of a faculty member.
ARA is funding awards under two call for proposals: Alexa Fairness in AI and AWS Automated Reasoning. Proposals were reviewed for the quality of their scientific content, their creativity, and their potential to impact both the research community, and society more generally. Theoretical advances, creative new ideas, and practical applications were all considered.
Recipients have access to more than 250 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.
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.
“Research in automated reasoning is deeply intertwined with a broad range of other research areas, touching machine learning, hardware and software engineering, robotics, and life sciences,” said Daniel Kroening, senior principal scientist for the Automated Reasoning Group. “The 2021 Amazon Research Awards reflect this breadth, and the interdisciplinary nature of research that is necessary to take computing one step closer to that magic spark that drives human reasoning.”
ARA funds proposals up to four times a year in a variety of research areas. Applicants are encouraged to visit the ARA call for proposals page for more information or send an email to be notified of future open calls.
Below is the list of Spring 2021 award recipients, presented in alphabetical order.
| Recipient | University | Research title |
| Haniel Barbosa | Universidade Federal de Minas Gerais | Efficient Checking and Reconstruction of SMT Proofs |
| Clark Barrett | Stanford University | HydraScale: Solving SMT Queries in the Serverless Cloud |
| Yuriy Brun | University of Massachusetts Amherst | Formal Verification via Language-Modeling-Based Proof Synthesis |
| Adam Chlipala | Massachusetts Institute of Technology | Correct-by-Construction IoT Systems and Cloud Servers |
| Jyotirmoy Deshmukh | University of Southern California | Systematic Testing and Invariant Synthesis for Concurrent Programs using Deep Reinforcement Learning |
| Isil Dillig | The University of Texas at Austin | Automated Code Modernization and Migration |
| Parasara Sridhar Duggirala | University of North Carolina at Chapel Hill | Model Checking For Counterexamples |
| Philippa Gardner | Imperial College London | A Multi-language Platform for Symbolic Testing and Verification |
| Jan Hoffmann | Carnegie Mellon University | Automatic Static Resource Analysis for Serverless Computing |
| Falk Howar | Technical University of Dortmund | Scaling Dynamic Symbolic Execution for Java |
| Anthony Lin | University of Kaiserslautern | Certified Solvers and Proof Checkers forString Constraints |
| Magnus Madsen | Aarhus University | Type Inference with Boolean Unification |
| Kuldeep S. Meel | National University of Singapore | GPU-Enabled Parallel SAT Solving |
| Eric Mercer | Brigham Young University | Symbolic Execution for Generating Java Tests from Dafny Models |
| Peter Müller | ETH Zurich | Verification of Rust Programs against TLA+ Specifications |
| Suha Orhun Mutluergil | Sabanci University | Linearizability Checking Via Symbolic Reasoning |
| Jason Nieh | Columbia University | Verifying System Software on an Arm Multiprocessor Hardware Model |
| Gennaro Parlato | University of Molise | Program Analysis in the Clouds (PAC): A Distributed Symbolic Algorithm to Scale Up Bug-finding in Concurrent Programs |
| Ruzica Piskac | Yale University | Counterexample-Guided Inference of Modular Specifications |
| Roopsha Samanta | Purdue University, West Lafayette | Automated and Modular Parameterized Verification of Distributed Systems (3225) |
| Sanjit Seshia | University of California, Berkeley | Scalable Verification of Secure Distributed Services through Synthesis and Learning |
| Alexander Summers | The University of British Columbia | Enriched Type and Memory Encodings for Modular Rust Verification |
| Josef Urban | Czech Technical University in Prague | Combining Neural and Symbolic Methods in Theorem Proving |
| Diyi Yang | Georgia Institute of Technology | Towards Dialect-Robust and Inclusive Natural Language Understanding |
| Qirun Zhang | Georgia Institute of Technology | Software Model Checking via Interleaved Dyck-Reachability |
| Danyang Zhuo | Duke University | Push-Button Verification of Software Middleboxes |
