Automated Reasoning call for proposals — Fall 2022
Systems assurance by mathematical proof
About this CFP
Amazon Science 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 provides higher assurance for customers—both about the cloud itself and about their data in the cloud. We anticipate funding research in these categories:
- Software verification, e.g., C, Rust, Java
- Improvements to SAT, SMT, and CHC solvers
- Model checking
- Correct-by-construction software
- Novel applications of automated reasoning
- Theorem proving
- Abstract interpretation
- Static analysis
- Efficient reasoning with quantifiers
- Automated reasoning
Submission period: September 16 to October 26, 2022
Decision letters will be sent out March 2023.
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
Awards 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 FAQ 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 and industry code.)
- What are potential applications of your work?
- 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:
- What license is your tool released under?
- What on-boarding/tutorial material is available?
- Is your tool actively maintained (commits within last 3 months)? How many active contributors does your project have?
ARA funding decisions will be based on potential impact to Amazon, 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 students working on automated reasoning at the undergraduate and graduate levels. 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.