API-driven Program Synthesis for Testing Static Typing Implementations
summary
Thalia synthesizes small, type‑intensive client programs from real libraries by building an API graph and enumerating typing sequences that drive component-based synthesis; it supports parametric polymorphism, overloading and higher‑order functions, offers fault‑injection and semantics‑preserving modes, and fills holes with API-derived expressions and constants. The tool finds 84 typing bugs (61 unexpected rejects, six soundness errors, 15 crashes, two performance regressions), produces tests of 11–30 lines, scales to API graphs >25k edges, and synthesizes programs in milliseconds.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:23Type checker bug examples
- 3:40Thalia system design
- 8:42Typing sequences for methods
- 10:27Concretizing test programs
- 11:10Evaluation results
- 13:19Comparison with tools
- 14:42Key insights
- 15:05Conclusion
- 15:28Q&A
related talks
24mEffective API schemas testing
42mIf I unit test do I really need static typing
28mLanguage Support for Property-Based Testing
31mAdventures in not writing tests
45mTDD, as in Type-Directed Development
19mCrabtree: Rust API Test Synthesis Guided by Coverage and Type
56mThe Rational Programmer, An Investigative Method for Programming Language Prag...
19mCovering All the Bases: Type-Based Verification of Test Input Generators