Automated Reasoning Call for Proposals — Fall 2023
Systems assurance by mathematical proof
About this CFP
Amazon is committed to helping customers achieve the highest levels of security, availability, and robustness in the cloud. Automated reasoning is the application of mathematical logic to answer questions and prove properties about critical computer systems. Using automated reasoning, Amazon is able to detect previously missed misconfigurations, or show their absence, and to prove that protocols and programs work as intended. Our work in provable security and privacy aims to provides higher assurance for customers. We anticipate funding research in these categories:
- Automated reasoning
- Abstract interpretation
- Correct-by-construction software
- Efficient reasoning with quantifiers
- Improvements to SAT, SMT, and CHC solvers
- Model checking
- Novel applications of automated reasoning
- Provable Privacy
- Software synthesis and optimization
- Software verification, e.g., C, Rust, Java
- Static analysis
- Theorem proving
- The use of automated reasoning to improve generative AI techniques
- Using automated reasoning in combination with generative AI techniques
- Verification of distributed protocols and systems
- Verification of randomized algorithms
Submission period: September 21, 2023 - November 13, 2023 (11:59PM Pacific Time)
Decision letters will be sent out March 2024
Selected Principal Investigators (PIs) may receive the following:
- Unrestricted funds, no more than $80,000 USD on average
- AWS Promotional Credits, no more than $20,000 USD on average
- Training resources, including AWS tutorials and hands-on sessions with Amazon scientists and engineers
Amazon Research Awards (ARA) are structured as one-year unrestricted gifts. The budget should include a list of expected costs specified in USD, and should not include administrative overhead costs. The final award amount will be determined by the awards panel.
Please refer to the ARA Program rules on the Rules and Eligibility page.
Proposals should be prepared according to the proposal template. Proposals should answer the following questions:
- Does your work target analysis of protocols, code, or configuration? Please provide information about your domain and the type of analysis.
- What are the current applications of your work? (e.g., libraries, codebases, or industry code).
- What are potential applications of your work to Amazon?
- What assumptions are made by your work? If the techniques proposed are sound: What are issues that may invalidate this result?
- If your work involves the development and maintenance of a tool:
- Under what license is or will your tool be released?
- What on-boarding/tutorial material is available?
- Is your tool actively maintained (i.e., commits within last 3 months)? How many active contributors does your project have?
ARA funding decisions will be based on potential impact to automated reasoning research, and the development of the automated reasoning scientific community. Amazon's commitment to developing the automated reasoning scientific community includes increasing the number of university researchers engaged in automated reasoning research. We are also committed to increasing the diversity of the automated reasoning community at all levels.
Expectations from recipients
To the extent deemed reasonable, Award recipients should acknowledge the support from ARA. Award recipients will inform ARA of publications, presentations, code and data releases, blogs/social media posts, and other speaking engagements referencing the results of the supported research or the Award. Award recipients are expected to provide updates and feedback to ARA via surveys or reports on the status of their research. Award recipients will have an opportunity to work with ARA on an informational statement about the awarded project that may be used to generate visibility for their institutions and ARA.