Steve Zdancewic
Department of Computer and Information Science
University of Pennsylvania

e-mail: stevez (at)
phone: 215-898-2661
office: 511 Levine Hall
office hours: Monday 3:30-5:00pm & by appointment
[Curiculum 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 randomized algorithms, type-directed program synthesis, linear types and GUI programming. 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 also 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.

Research Projects and Activities

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.

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.


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.


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)

  • Programming Languages and Techniques I (CIS 120)
    2017 2016, 2014, 2012, 2011, 2010
  • Compilers (CIS 341)
    2017 , 2015, 2013, 2011, 2008
  • Software Foundations (CIS 500)
    2016, 2013
  • Software and Compiler Verification (CIS 700)
  • Computer and Network Security (CIS 551)
    2012 , 2009 , 2008 , 2007 , 2006 , 2005
  • Introduction to Networks and Security (CSE 331)
    2006 , 2004 , 2003 , 2002
  • π-Calculus and Foundations of Concurrent Systems (CIS 700)
  • Advanced Topics in PL: Safety and Security (CIS 670)


Current Ph.D. Students and Post Docs

Former Students and Post Docs

Awards and Honors

  • 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


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

Last modified: Thu Aug 17 14:33:33 EDT 2017