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 22:10:44 GMT cache-control: max-age=600 content-encoding: gzip x-proxy-cache: MISS x-github-request-id: D2DA:2F7ECD:95A46B:A7E6CA:6952FA0B accept-ranges: bytes age: 0 date: Mon, 29 Dec 2025 22:00:44 GMT via: 1.1 varnish x-served-by: cache-bom-vanm7210058-BOM x-cache: MISS x-cache-hits: 0 x-timer: S1767045644.999662,VS0,VE208 vary: Accept-Encoding x-fastly-request-id: 01916e349b35bfeedb6698156290cf9165b81952 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.