Principal Applied Scientist
Automated Reasoning Group
I am a principal applied scientist at the Automated Reasoning Group at Amazon's Simple Storage Service (S3-ARG). I took a founding role in the first Automated Reasoning (AR) Group at AWS, first leading a team working on the "security of the cloud" (focusing on AWS internals). This team evolved into one developing tools and collaborating with teams in IoT, cryptography, Identity and Access Management, and S3 to integrate our tools into their design and implementation processes. I started S3-ARG, S3's dedicated AR team in 2020. S3-ARG works on all aspects of correctness and durability for S3, an extremely complex and large distributed system. (We are hiring!) See this talk on our work on S3 strong consistency and the coverage of our work in Peter DeSantis's re:Invent 2021 keynote.
My current technical interests are in model-based testing of web service APIs and checking conformance of code implementing distributed systems to design models. Bridging implementations and models/specifications in this manner increases confidence in the correctness of implementations and provides a mechanism for code and models to remain in sync. Throughout my career, I have focused on concurrent systems implemented in hardware and/or software. I have both developed static, compositional proof methods and worked on dynamic/runtime techniques (including supporting a proposed DataRaceException in Java). At S3-ARG, we are developing and deploying a wide variety of automated reasoning methods that help us strike the compromises between ease-of-use/automation and degree of assurance we need for each application.
I received my MS and PhD from the University of California at Berkeley in 1995 and 1998 respectively. 1998-2000, I was a research scientist at the Gigascale Systems Research Center. From 2000-2003, I was a research scientist at the DEC/Compaq/HP Systems Research Center (SRC). 2003-2016, I was a professor at Koç University, Istanbul, Turkey. While at Koç University, I collaborated closely with (and was funded by) Microsoft Research, and had visiting appointments at Microsoft Research (Redmond, Cambridge, Bangalore), Univ. Paris VI, Univ. Paris VII, MIT, and EPFL. I am a Distinguished Research Fellow at Sabanci University, Istanbul, Turkey, and on the advisory board for computer engineering at Koc University.
Selected Publications at Amazon
Using lightweight formal methods to validate a key-value storage node in Amazon S3 (SOSP 2021 best paper)
A Machine-Checked Proof of Security for AWS Key Management Service, (CCS 2019)
Continuous Formal Verification of Amazon s2n (CAV 2018, honorable mention in NSA cybersecurity paper competition)
A solver-aided language for test input generation. (OOPSLA 2017)
Selected Publications prior to Amazon
Automated and Modular Refinement Reasoning for Concurrent Programs (CAV 2015)
A Calculus of Atomic Actions (POPL 2009)
Goldilocks: A Race-Aware Java Runtime (CACM Research Highlights 2010, PLDI 2007)
VYRD: verifYing concurrent programs by runtime refinement-violation detection (PLDI 2005)
Using a formal specification and a model checker to monitor and direct simulation:
Verifying the Multiprocessing Hardware of the Alpha 21364 Multiprocessor (DAC 2003)
An assume-guarantee rule for checking simulation (TOPLAS 2002)
Coverage Metrics for Functional Validation of Hardware Designs (IEEE Design&Test 2001)
MOCHA: Modularity in Model Checking (CAV 1998)
Verifying Abstractions of Timed Systems (CONCUR 1996)
All publications can be found here.