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 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.