Serdar Tasiran
Principal Applied Scientist
Automated Reasoning Group, Agentic AI, AWS
serdar@berkeley.edu
Embedded Files
I am a principal applied scientist at Amazon, in the Agentic AI Automated Reasoning Group. I work on neurosymbolic techniques to formally verify correctness, security, and operational safety properties of AI-generated code and cloud infrastructure as code.
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 the Simple Storage Service (S3) to integrate our tools into design and implementation processes. I started and led S3-ARG, S3's dedicated AR team in 2020 before I moved to the Agentic AI organization.
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 science at Sabanci University. I am a member of the IFIP Working Group WG 2.3 on Programming Methodology.
Publications at Amazon
N. Jaber, D. Jin, B. Kragl, E. Magnago, G. Petri, T. Tarrach, S. Tasiran. “High Fidelity Models for Large Scale Stateful Services.” In Proc. 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2026).
A. Chakarov, J. Geldenhuys, M. Heck, M. Hicks, S. Huang, G. Jaloyan, A. Joshi, R. Leino, M. Mayer, S. McLaughlin, A. Mritunjai, C. Pit-Claudel, S. Porncharoenwase, F. Rabe, M. Rapoport, G. Reger, C. Roux, N. Rungta, R. Salkeld, M. Schlaipfer, D. Schoepe, J. Schwartzentruber, S. Tasiran, A. Tomb, E. Torlak, J. Tristan, L. Wagner, M. Whalen, R. Willems, J. Xiang, T. Byun, J. Cohen, R. Wang, J. Jang, J. Rath, H. Syeda, D. Wagner, Y. Yuan. “Formally Verified Cloud-Scale Authorization.” In Proc. 47th International Conference on Software Engineering (ICSE 2025). https://amazon.science/publications/formally-verified-cloud-scale-authorization — ACM SIGSOFT Distinguished Paper Award.
J. Bornholt, R. Joshi, V. Astrauskas, B. Cully, B. Kragl, S. Markle, K. Sauri, D. Schleit, G. Slatton, S. Tasiran, J. Van Geffen, A. Warfield. “Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3.” In Proc. 28th ACM Symposium on Operating Systems Principles (SOSP 2021). https://dl.acm.org/doi/10.1145/3477132.3483540 — Distinguished Paper Award.
N. Chong, B. Cook, J. Eidelman, K. Kallas, K. Khazem, F. Monteiro, D. Schwartz-Narbonne, S. Tasiran, M. Tautschnig, M. Tuttle. “Code-Level Model Checking in the Software Development Workflow at Amazon Web Services.” In Proc. 42nd International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP 2020). https://dl.acm.org/doi/abs/10.1145/3377813.3381347.
M. Kellogg, M. Schäf, S. Tasiran, M. Ernst. “Continuous Compliance.” In Proc. 35th IEEE/ACM International Conference on Automated Software Engineering (ASE 2020), pp. 511–523.
J. Almeida, M. Barbosa, G. Barthe, M. Campagna, E. Cohen, B. Gregoire, V. Pereira, B. Portela, P. Strub, S. Tasiran. “A Machine-Checked Proof of Security for AWS Key Management Service.” In Proc. ACM Conference on Computer and Communications Security (CCS 2019), pp. 63–78. https://dl.acm.org/doi/10.1145/3319535.3363211.
I. Dillig and S. Tasiran (Eds.). Computer Aided Verification (CAV 2019). Lecture Notes in Computer Science, vol. 11561–11562. Springer, 2019. https://link.springer.com/book/10.1007/978-3-030-25540-4 — Conference co-chair; proceedings editor.
A. Chudnov, N. Collins, B. Cook, J. Dodds, B. Huffman, C. MacCárthaigh, S. Magill, E. Mertens, E. Mullen, S. Tasiran, A. Tomb, E. Westbrook. “Continuous Formal Verification of Amazon s2n.” In Proc. 30th International Conference on Computer Aided Verification (CAV 2018), LNCS 10981, pp. 642–654. Springer. https://link.springer.com/chapter/10.1007/978-3-319-96142-2_26 — NSA Best Scientific Cybersecurity Paper recognition.
B. Cook, K. Khazem, D. Kroening, S. Tasiran, M. Tautschnig, M. Tuttle. “Model Checking Boot Code from AWS Data Centers.” In Proc. 30th International Conference on Computer Aided Verification (CAV 2018), LNCS 10981. Springer. https://www.amazon.science/publications/model-checking-boot-code-from-aws-data-centers.
K. Athanasiou, B. Cook, M. Emmi, C. MacCarthaigh, D. Schwartz-Narbonne, S. Tasiran. “SideTrail: Verifying Time-Balancing of Cryptosystems.” In Proc. 10th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2018), LNCS 11294. Springer. https://link.springer.com/doi/10.1007/978-3-030-03592-1_12.
D. Cok and S. Tasiran. “Practical Methods for Reasoning About Java 8’s Functional Programming Features.” In Proc. 10th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2018), LNCS 11294. Springer. https://link.springer.com/doi/10.1007/978-3-030-03592-1_15.
T. Ringer, D. Grossman, D. S-Narbonne, S. Tasiran. “A solver-aided language for test input generation.” Proc. ACM Program. Lang. 1(OOPSLA): 91:1-91:24 (2017) https://dl.acm.org/doi/10.1145/3133915
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)
Page updated
Google Sites
Report abuse