|
Steve ZdancewicSchlein Family President’s Distinguished Professor e-mail: stevez (at) cis.upenn.edu |
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.
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.
Concurrent LLVM Equivalence Analysis through Refinement, in conjunction with Galois Inc., is part of the DARPA TRACTOR program, which aims to automate the translation of legacy C code to Rust.
I served as General Chair for POPL 2025, held in Denver, Colorado.
The DeepSpec project focused on the specification and verification of full functional correctness of software and hardware, bringing Coq formalization to bear on systems-level programs such as compilers, operating systems, and databases.
The goal of this project was to devise novel methods for ensuring that quantum programs are correct, addressing the challenge that quantum algorithms explore alternative computation branches in superposition.
This NSF Expedition on Computer-Augmented Program Engineering sought to transform the way that programmers develop software by advancing the theory and practice of software synthesis.
This project developed software instrumentation techniques to achieve complete memory safety for C programs, while requiring minimal changes to the source programs.
This research sought to develop programming language abstractions and analyses that let developers create programs that are secure by construction.
CIS 120/1200: Programming Languages and Techniques I
University of Pennsylvania — Fall 2010, 2011, 2012, 2014, 2016, 2017, 2019, 2020, 2021, 2023 Spring, 2023 Fall, 2025
A freshman-level undergraduate course that introduces the basics of programming and computer science.
CSE 331: Introduction to Networks and Security
University of Pennsylvania — Fall 2002, 2003, 2004, 2006
A junior and senior level undergraduate course that introduces the fundamentals of network and computer security, basic cryptographic protocols, and secure system design.
CIS 4521/5521: Compilers and Interpreters
University of Pennsylvania — Spring 2025
An advanced undergraduate/graduate level course that introduces compiler design and implementation. (Formerly CIS 341/3410.)
CIS 341/3410: Compilers and Interpreters
University of Pennsylvania — Fall 2008; Spring 2011, 2013, 2015, 2017, 2018, 2020, 2022, 2024
A junior and senior undergraduate level course that introduces compiler design and implementation.
CIS 500/5000: Software Foundations
University of Pennsylvania — Fall 2013, 2022, 2024; Spring 2016
A graduate level course that covers formal logic, programming language semantics, and reasoning about software.
CIS 551: Computer and Network Security
University of Pennsylvania — Spring 2005, 2006, 2007, 2008, 2009, 2012
A graduate level course that covers software, system, and network security, including: buffer-overflow attacks, denial of service attacks, cryptographic protocols, and countermeasures.
CIS 670: Advanced Topics in Programming Languages: Safety and Security
University of Pennsylvania — Spring 2003, Spring 2014
A graduate level course on the topics of advanced language design, type systems, and program analyses as they apply to safety and security of software.
CIS 670: Advanced Topics in Programming Languages
University of Pennsylvania — Spring 2021
A graduate level course on the topics of advanced language design and type systems, concentrating on: polymorphic lambda calculus, parametricity and logical relations, linear types, and modern applications of these ideas in programming languages like Rust.
CIS 700: Software and Compiler Verification
University of Pennsylvania — Fall 2005
A graduate seminar that surveyed the historic and current approaches to verifying compilation, focusing on the programming language and compiler aspects of the problem.
CIS 700: $\pi$-Calculus and the Foundations of Concurrent Systems
University of Pennsylvania — Spring 2004
Co-taught with Benjamin Pierce.
A graduate seminar that introduced Milner’s $\pi$-calculus as a tool for studying key features of concurrent systems, including synchronization and message passing.
CIS 7000: Compilers
University of Pennsylvania — Spring 2024
Experimental offering of CIS 3410 as a masters-level course.
