Award Recipient Armando Solar-Lezama Massachusetts Institute of Technology 2025 Amazon Research Award Synthesizing Library Models for Static Analysis via LLMs and Conformance Testing Research topic Automated reasoning