معرفی
Steve Zdancewic is the Schlein Family President's Distinguished Professor and Associate Chair in the Department of Computer and Information Science at the University of Pennsylvania. His research spans programming languages, computer security, formal verification, and type theory, with significant contributions to LLVM verification, program synthesis, and quantum programming. He co-leads Penn's Programming Languages Research Group with Benjamin Pierce and Stephanie Weirich.
His research focuses on:
- Programming language foundations (type theory, linear logic, semantics)
- Formal verification (Coq, LLVM, interaction trees)
- Security (information-flow control, memory safety)
- Emerging paradigms (quantum programming, secure distributed systems)
Publication trends reveal deep engagement with formal methods (67%), programming language design (20%), and systems security (13%), primarily using Coq for mechanized verification. Recent works demonstrate increased focus on parallel/streaming computation and synthesis techniques.
Awards
- Distinguished Paper Awards (ECOOP 2023, POPL 2020)
- Schlein Family President's Distinguished Professor (2021)
- Lindback Distinguished Teaching Award (2018)
- IEEE MICRO Top Picks (2013)
- Sloan Fellowship (2009-2010)
- NSF CAREER Award (2004)
- Best Paper Awards (SOSP 2001, ICFP 1999)
Research Leadership
Directs multiple NSF-funded projects including DeepSpec (verified systems infrastructure), Vellvm (LLVM semantics), and ExCAPE (program synthesis). Advises 5 PhD students and 31 former advisees/postdocs. Served as General Chair for POPL 2025 and associate chair for PLDI/ICFP/POPL.
Infrastructure
Leads the Vellvm project developing Coq-based LLVM semantics, the Interaction Trees framework for recursive/impure programs, and Qwire for quantum circuit verification. Maintains active collaborations with Galois Inc. and INRIA.
