Colloquium: Automated Logic-Based Reasoning for Analyzing Prime Video Code

Title: Automated Logic-Based Reasoning for Analyzing Prime Video Code

Abstract: Developers working in Prime Video are constantly innovating, introducing new features, and improving the performance of the Prime Video application. Each modification of the Prime Video application code is required to pass a testing and code review process before it is delivered to customer devices. As the application evolves rapidly, it cannot be expected that manual reasoning about the code keeps up with the software complexity curve. This setting presents an opportunity for the application of automated logic-based approaches. In this talk, we present techniques and tools we have used and developed in order to automatically reason about the Prime Video application code. We discuss a code review bot, which runs multiple static code analysis tools, and introduce a novel static analyzer for TypeScript, which enables reasoning about deep properties in a trustworthy manner, while providing transparent actionable feedback to the developers.

Bio Ilina is an Applied Scientist at Prime Video working on applying automated reasoning techniques, currently developing a static code analyzer for TypeScript programs using abstract interpretation. She obtained her PhD from TU Wien in Vienna, Austria, where she developed methods for automatic verification of synchronous fault-tolerant distributed algorithms. Prior to joining Amazon, she was a research engineer at Informal Systems, where she worked on formally specifying and verifying blockchain protocols using TLA+.