Steve Zdancewic
Schlein Family President's Distinguished Professor and Associate Chair
Department of Computer and Information Science
University of Pennsylvania

e-mail: stevez (at) cis.upenn.edu
phone: 215-898-2661
office: 511 Levine Hall
office hours: Monday 3:30-5:00pm & by appointment
[Curriculum Vitae]             [Publications]             [Teaching]             [Students]

Research Interests

I study programming languages and computer security. I have wide-ranging interests, and some of my most recent work touches on: Coq verification of LLVM program transformations and quantum circuits, type-directed program synthesis, linear types and verified web server implementations. I have also spent a lot of time thinking about language-based enforcement of information-flow policies, low-level code memory safety, understanding dynamic security policies, and authorization logic. I am interested in secure concurrent and distributed computing, functional programming languages, type theory, linear and modal logics, theorem proving and mechanized metatheory. More information about my research can be found in this (out of date) research statement.


Current Research Projects and Activities

POPL 2025

I am the General Chair for POPL 2025, which will be held in Denver, Colorado. Submit a paper! Attend the meeting!

PL Club

Penn's programming languages research group, run jointly with Benjamin Pierce and Stephanie Weirich. We meet weekly with students and post-docs to discuss current research topics.

Vellvm

The verified LLVM project is developing operational semantics for the LLVM intermediate representation using the interactive theorem prover Coq. The resulting tools let us create highly-reliable program transformation passes and optimizations.

Vellvm Coq development

Previous Research Projects and Activities

NSF Expedition on the Science of Deep Specification

The DeepSpec project focuses on the specification and verification of full functional correctness of software and hardware. We are bringing Coq formalization to bear on systems-level programs such as compilers, operating systems, and databases.

Interaction Trees Coq development

Semantics, Formal Reasoning, and Tools for Quantum Programming

Quantum algorithms are complex, and quantum computers explore alternative computation branches in superposition, so programming mistakes in even minor parts of the code can alter the quantum state and invalidate the final result. The goal of this project is to devise novel methods for ensuring that quantum programs are correct.

QWIRE Coq development

ExCAPE

This NSF Expedition on Computer-Augmented Program Engineering seeks to transform the way that programmers develop software by advancing the theory and practice of software synthesis.

SoftBound + CETS

This project is developing software instrumentation techniques to achieve complete memory safety for C programs, while requiring minimal changes to the source programs.

Security-Oriented Languages

This research seeks to develop programming language abstractions and analyses that let developers create programs that are secure by construction.


Recent Publications (Complete List)


Teaching (Summary)


Advising

Current Ph.D. Students

Former Students and Post Docs


Awards and Honors

  • Distinguished Paper Award for Semantics for Noninterference with Interaction Trees ECOOP 2023
  • Endowed Chair: Schlein Family President's Distinguished Professor, 2021
  • Distinguished Paper Award for Interaction Trees POPL 2020
  • Christian R. and Mary F. Lindback Foundation Award for Distinguished Teaching, 2018
  • IEEE MICRO "top picks", 2013
  • Alfred P. Sloan Fellow, 2009-2010
  • NSF CAREER award, 2004
  • Best Paper award at SOSP, 2001
  • Intel Foundation Graduate Fellowship, 2001
  • Best Paper award at ICFP, 1999
  • NSF Graduate Student Fellowship, 1996


Talks

Some of my old talks are available:

Miscellany

  • My wife, Stephanie Weirich, is also on the Computer and Information Science Faculty at Penn.
  • At some point I wrote up some writing tips for Ph.D. students.