Type-Guided Worst-Case Input Generation

The following summary was generated by AI from the slides.

Type-Guided Worst-Case Input Generation (Di Wang and Jan Hoffmann, POPL 2019) combines AARA-derived resource types with worst-case execution-path search to automatically produce concrete inputs that drive a program to its maximum resource consumption, with applications including Denial-of-Service vulnerability discovery, timing side-channel analysis, and blockchain gas-cost auditing. Static resource analysis — exemplified by Infer’s cost checker, which reports bounds such as and detects complexity increases to upon code changes — provides sound, modular, compile-time bounds over all inputs without requiring test execution. The key insight is that AARA potential annotations, which encode how much cost is stored in data structures, directly guide the worst-case execution-path search, making it substantially more efficient than naive enumeration.