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 provide higher assurance for customers. We anticipate funding research in these categories:
- Automated reasoning
- Abstract interpretation
- Correct-by-construction software
- Dafny
- 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
https://www.amazon.science/research-awards/call-for-proposals/automated-reasoning-call-for-proposals-fall-2023