HTTP/2 200 server: GitHub.com content-type: text/html; charset=utf-8 last-modified: Fri, 13 Jun 2025 22:06:08 GMT access-control-allow-origin: * etag: W/"684ca0d0-992" expires: Mon, 29 Dec 2025 03:59:11 GMT cache-control: max-age=600 content-encoding: gzip x-proxy-cache: MISS x-github-request-id: 13BF:444BC:8449A6:94A026:6951FA36 accept-ranges: bytes age: 0 date: Mon, 29 Dec 2025 03:49:11 GMT via: 1.1 varnish x-served-by: cache-bom-vanm7210081-BOM x-cache: MISS x-cache-hits: 0 x-timer: S1766980152.541591,VS0,VE201 vary: Accept-Encoding x-fastly-request-id: c55351bef733a58d0737d106f4d80093593cbd82 content-length: 1134

Emina Torlak

Senior Principal Scientist at Amazon Web Services
Affiliate Professor at University of Washington

My research aims to help people build better software more easily. I develop languages and tools for program verification and synthesis. I created Rosette and Kodkod, and lead the design and development of Cedar. Rosette is a solver-aided language that powers verification and synthesis tools for all kinds of systems, from radiation therapy control to Linux JIT compilers. Kodkod is a solver for relational logic, used widely in tools for software analysis and design. Cedar is an expressive, fast, and analyzable language for authorization, used by cloud services such as Amazon Verified Permissions and AWS Verified Access.