Photo of Emina by Dennis Wise

Emina Torlak

Senior Principal Scientist at Amazon Web Services

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 co-lead the development of Cedar (with Mike Hicks). 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 Amazon Verified Permissions and AWS Verified Access.