Steve Zdancewic's Publications
Copyright Information
|
Journal Articles
[1]
|
Stephen Mell, Steve Zdancewic, and Osbert Bastani.
Optimal Program Synthesis via Abstract Interpretation.
8(POPL), 2024.
[ PDF
Abstract ]
|
[2]
|
Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic.
Choice Trees: Representing Nondeterministic, Recursive, and
Impure Programs in Coq.
Proceedings of the ACM on Programming Languages, 7(POPL), 2023.
[ PDF
Abstract ]
|
[3]
|
Nick Rioux, Xuejing Huang, Bruno C. d. S. Oliviera, and Steve Zdancewic.
A Bowtie for a Beast: Overloading, Eta Expansion, and
Extensible Data Types in F.
Proceedings of the ACM on Programming Languages, 7(POPL), 2023.
[ PDF
Abstract ]
|
[4]
|
Mohsen Lesani, Li-Yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala,
Benjamin C. Pierce, and Steve Zdancewic.
C4: Verified Transactional Objects.
Proceedings of the ACM on Programming Languages, OOPSLA, 2022.
[ PDF
Abstract ]
|
[5]
|
Irene Yoon, Yannick Zakowski, and Steve Zdancewic.
Formal Reasoning About Layered Monadic Interpreters.
Proceedings of the ACM on Programming Languages, 6(ICFP), 2022.
[ PDF
Abstract ]
|
[6]
|
Lucas Silver and Steve Zdancewic.
Dijkstra Monads Forever: Termination-Sensitive Specifications
for Interaction Trees.
Proceedings of the ACM on Programming Languages, 5(POPL),
January 2021.
[ PDF
Abstract ]
|
[7]
|
Yannick Zakowski, Calvin Beck, Irene Yoon, Ilya Zaichuk, Vadim Zaliva, and
Steve Zdancewic.
Modular, Compositional, and Executable Formal Semantics for LLVM
IR.
Proceedings of the ACM on Programming Languages, 5(ICFP), 2021.
[ PDF
Abstract ]
|
[8]
|
Paul He, Eddy Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl
Smeltzer, Andrei Andrei Ştefănescu, Aaron Tomb, Adam Wick, Matthew
Yacavone, and Steve Zdancewic.
A Type System for Extracting Functional Specifications from
Memory-Safe Imperative Programs.
Proceedings of the ACM on Programming Languages, OOPSLA, 2021.
[ PDF
Abstract ]
|
[9]
|
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha,
Benjamin C. Pierce, and Steve Zdancewic.
Interaction Trees.
Proceedings of the ACM on Programming Languages, 4(POPL),
January 2020.
[ PDF
Abstract ]
|
[10]
|
Nick Rioux and Steve Zdancewic.
Computation Focusing.
Proceedings of the ACM on Programming Languages, 5(ICFP), 2020.
[ PDF
Abstract ]
|
[11]
|
Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David
Walker, and Steve Zdancewic.
Synthesizing Symmetric Lenses.
Proceedings of the ACM on Programming Languages, 3(ICFP), 2019.
[ PDF
Abstract ]
|
[12]
|
Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve
Zdancewic.
Synthesizing Bijective Lenses.
Proceedings of the ACM on Programming Languages, 2(POPL),
January 2018.
[ PDF
Abstract ]
|
[13]
|
Solomon Maina, Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David
Walker, and Steve Zdancewic.
Synthesizing Quotient Lenses.
Proceedings of the ACM on Programming Languages, 2(ICFP), 2018.
[ PDF
Abstract ]
|
[14]
|
Andrew W. Appel, Lennart Beringer, Adam Chlipala, Benjamin C. Pierce, Zhong
Shao, Stephanie Weirich, and Steve Zdancewic.
Position paper: The Science of Deep Specification.
Philosophical Transactions of the Royal Society of London A:
Mathematical, Physical and Engineering Sciences, 375(2104), 2017.
[ DOI
http
Abstract ]
|
[15]
|
B. Valiron and S. Zdancewic.
Modeling Simply-Typed Lambda Calculi in the Category of Finite
Vector Spaces.
Scientific Annals of Computer Science, 24(2):325--368, 2014.
[ DOI
PDF
Abstract ]
|
[16]
|
Peng Li and Steve Zdancewic.
Arrows for Secure Information Flow.
Theoretical Computer Science, 411(19):1974--1994, 2010.
[ PDF
Abstract ]
|
[17]
|
Stephen Tse and Steve Zdancewic.
Run-time principals in information-flow type systems.
Transactions on Programming Languages and Systems, 30(1):6,
2008.
[ PDF
Abstract ]
|
[18]
|
Andrew C. Myers, Andrei Sabelfeld, and Steve Zdancewic.
Enforcing Robust Declassification and Qualified Robustness.
Journal of Computer Security, 14(2):157--196, 2006.
[ PDF
Abstract ]
|
[19]
|
Jay Ligatti, David Walker, and Steve Zdancewic.
A Type-theoretic Interpretation of Pointcuts and Advice.
Science of Computer Programming: Special Issue on Foundations of
Aspect-Oriented Programming, pages 240--266, 2006.
[ PDF
Abstract ]
|
[20]
|
Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, and Andrew C. Myers.
Secure Program Partitioning.
Transactions on Computer Systems, 20(3):283--328, 2002.
[ PDF
PS
Abstract ]
|
[21]
|
Steve Zdancewic and Andrew C. Myers.
Secure Information Flow via Linear Continuations.
Higher Order and Symbolic Computation, 15(2/3):209--234, 2002.
[ PDF
PS
Abstract ]
|
[22]
|
Dan Grossman, Greg Morrisett, and Steve Zdancewic.
Syntactic Type Abstraction.
Transactions on Programming Languages and Systems,
22(6):1037--1080, November 2000.
[ PDF
PS
Abstract ]
|
|
Invited Papers
[1]
|
Steve Zdancewic.
Challenges for Information-flow Security.
In Proceedings of the 1st International Workshop on the
Programming Language Interference and Dependence (PLID'04), 2004.
(5 pages).
[ PDF ]
|
[2]
|
Steve Zdancewic.
A Type System for Robust Declassification.
In Proceedings of the Nineteenth Conference on the Mathematical
Foundations of Programming Semantics (MFPS). Electronic Notes in Theoretical
Computer Science, March 2003.
(16 pages).
[ PDF
PS
Abstract ]
|
|
Conference and Selective Workshop Papers
[1]
|
Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic.
Semantics for Noninterference with Interaction Trees.
In Proceedings of the 37th Annual European Conference on
Object-Oriented Programming (ECOOP 2023), 2023.
[ PDF
Abstract ]
|
[2]
|
Stephen Mell, Favyen Bastani, Steve Zdancewic, and Osbert Bastani.
Synthesizing Trajectory Queries from Examples.
In Computer Aided Verification - 35th International Conference,
CAV, 2023.
[ PDF
Abstract ]
|
[3]
|
Lawrence Dunn, Val Tannen, and Steve Zdancewic.
Syntax Monads for the Working Formal Metatheorist.
In Proceedings of the 6th International Conference on Applied
Category Theory (ACT), 2023.
[ PDF
Abstract ]
|
[4]
|
Lawrence Dunn, Val Tannen, and Steve Zdancewic.
Tealeaves: Structured Monads for Generic First-Order Abstract
Syntax Infrastructure.
In 14th International Conference on Interactive Theorem Proving
(ITP), 2023.
[ PDF
Abstract ]
|
[5]
|
George Tolkachev, Stephen Mell, Steve Zdancewic, and Osbert Bastani.
Counterfactual Explanations for Natural Language Interfaces.
In 60th Annual Meeting of the Association for Computational
Linguistics (ACL), 2022.
(short paper).
[ PDF
Abstract ]
|
[6]
|
Stephen Mell, Osbert Bastani, and Steve Zdancewic.
Ideograph: A Language for Expressing and Manipulating Structured
Data.
In Proceedings Twelfth International Workshop on Computing with
Terms and Graphs (TERMGRAPH 2022), pages 65--84. Electronic Proceedings in
Theoretical Computer Science, 2022.
[ PDF
Abstract ]
|
[7]
|
Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia,
Lennart Beringer, William Mansky, Benjamin Pierce, and Steve Zdancewic.
Verifying an HTTP Key-Value Server with Interaction Trees and
VST.
In Liron Cohen and Cezary Kaliszyk, editors, 12th International
Conference on Interactive Theorem Proving (ITP 2021), volume 193 of
Leibniz International Proceedings in Informatics (LIPIcs), pages
32:1--32:19, Dagstuhl, Germany, 2021. Schloss Dagstuhl -- Leibniz-Zentrum
für Informatik.
[ DOI
PDF
http
Abstract ]
|
[8]
|
Yishuai Li, Benjamin Pierce, and Steve Zdancewic.
Model-Based Testing of Networked Applications.
In The ACM SIGSOFT International Symposium on Software Testing
and Analysis (ISSTA), 2021.
[ Abstract ]
|
[9]
|
Yannick Zakowski, Paul He, Chung-Kil Hur, and Steve Zdancewic.
An Equational Theory for Weak Bisimulation via Generalized
Parameterized Coinduction.
In Proceedings of the 9th ACM SIGPLAN International Conference
on Certified Programs and Proofs (CPP), January 2020.
[ PDF
Abstract ]
|
[10]
|
Nicolas Koh, Yao Li, Yishuai Li, Li yao Xia, Lennart Beringer, Wolf Honoré,
William Mansky, Benjamin C. Pierce, and Steve Zdancewic.
From C to Interaction Trees: Specifying, Verifying, and Testing
a Networked Server.
In Proceedings of the 8th ACM SIGPLAN International Conference
on Certified Programs and Proofs (CPP), January 2019.
[ PDF
Abstract ]
|
[11]
|
Marcella Hastings, Brett Hemenway, Daniel Noble, and Steve Zdancewic.
SoK: General Purpose Compilers for Secure Multi-Party
Computation.
In IEEE 2019 Symposium on Security and Privacy (Oakland),
2019.
[ PDF
Abstract ]
|
[12]
|
Jennifer Paykin and Steve Zdancewic.
A HoTT Quantum Equational Theory.
In The 16th International Conference on Quantum Physics and
Logic (QPL), 2019.
extended version available on arXiv.
[ http
Abstract ]
|
[13]
|
Christine Rizkallah, Dmitri Garbuzov, and Steve Zdancewic.
A Formal Equational Theory for Call-By-Push-Value.
In 9th International Conference on Interactive Theorem Proving
(ITP), 2018.
[ PDF
Abstract ]
|
[14]
|
Robert Rand, Jennifer Paykin, Dong-Ho Lee, and Steve Zdancewic.
REQUIRE: Reasoning about Reversible Quantum Circuits.
In The 15th International Conference on Quantum Physics and
Logic (QPL), 2018.
[ PDF ]
|
[15]
|
Jennifer Paykin, Robert Rand, and Steve Zdancewic.
QWire: A Core Language for Quantum Circuits.
In Proc. of the ACM Symposium on Principles of Programming
Languages (POPL), 2017.
[ PDF
Abstract ]
|
[16]
|
William Mansky, Yuanfeng Peng, Steve Zdancewic, and Joseph Devietti.
Verifying Dynamic Race Detection.
In The 6th ACM SIGPLAN Conference on Certified Programs and
Proofs (CPP 2017), 2017.
[ PDF
Abstract ]
|
[17]
|
Robert Rand, Jennifer Paykin, and Steve Zdancewic.
Qwire Practice: Formal Verification of
Quantum Circuits in Coq.
In The 14th International Conference on Quantum Physics and
Logic (QPL), 2017.
[ PDF
Abstract ]
|
[18]
|
Jennifer Paykin and Steve Zdancewic.
The Linearity Monad.
In Proceedings of the 10th ACM SIGPLAN International Haskell
Symposium, 2017.
[ PDF
Abstract ]
|
[19]
|
Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic.
Example-Directed Synthesis: A Type-Theoretic Interpretation.
In Proc. of the ACM Symposium on Principles of Programming
Languages (POPL), 2016.
[ PDF
Abstract ]
|
[20]
|
Jennifer Paykin and Steve Zdancewic.
Linear λμ is CP (more or less).
In A List of Successes to Change the World (Wadlerfest), 2016.
[ PDF
Abstract ]
|
[21]
|
Peter-Michael Osera and Steve Zdancewic.
Type-and-Example-Directed Program Synthesis.
In Proc. 2015 ACM SIGPLAN Conference on Programming Languages
Design and Implementation (PLDI), 2015.
[ PDF
Abstract ]
|
[22]
|
Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic,
and Viktor Vafeiadis.
A Formal C Memory Model Supporting Integer-Pointer Casts.
In Proc. 2015 ACM SIGPLAN Conference on Programming Languages
Design and Implementation (PLDI), 2015.
[ PDF
Abstract ]
|
[23]
|
William Mansky, Dmitri Garbuzov, and Steve Zdancewic.
An Axiomatic Specification for Sequential Memory Models.
In Computer Aided Verification - 27th International Conference,
CAV 2015, 2015.
[ PDF
Abstract ]
|
[24]
|
Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic.
Everything You Want to Know About Pointer-Based Checking.
In 1st Summit on Advances in Programming Languages, SNAPL
2015, May 3-6, 2015, Asilomar, California, USA, pages 190--208, 2015.
[ DOI
PDF
http
Abstract ]
|
[25]
|
Robert Rand and Steve Zdancewic.
VPHL: A Verified Partial-Correctness Logic for Probabilistic
Programs.
In Mathematical Foundations of Program Semantics (MFPS), 2015.
[ PDF
Abstract ]
|
[26]
|
Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic.
WatchdogLite: Hardware-Accelerated Compiler-Based Pointer
Checking.
In Proceedings of Annual IEEE/ACM International Symposium on
Code Generation and Optimization, CGO '14, pages 175:175--175:184. ACM,
2014.
[ DOI
PDF
http
Abstract ]
|
[27]
|
Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic.
A Core Quantitative Coeffect Calculus.
In Proc. of the 23rd European Symposium on Programming (ESOP),
volume 8410, pages 351--370, 2014.
[ PDF
Abstract ]
|
[28]
|
Benoît Valiron and Steve Zdancewic.
Finite vector spaces as model of simply-typed lambda-calculi.
In Proceedings of the 11th International Colloquium on
Theoretical Aspects of Computing (ICTAC 14), 2014.
[ PDF
Abstract ]
|
[29]
|
Santosh Nagarakatte, Milo M K Martin, and Steve Zdancewic.
Hardware-enforced Comprehensive Memory Safety.
IEEE MICRO's "Top Picks of Architecture Conferences of 2012"
Issue (Micro Top Picks'2013), May/June 2013.
[ PDF
Abstract ]
|
[30]
|
Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic.
Formal Verification of SSA-Based Optimizations for LLVM.
In Proc. 2013 ACM SIGPLAN Conference on Programming Languages
Design and Implementation (PLDI), 2013.
[ PDF
Abstract ]
|
[31]
|
Christian DeLozier, Richard Eisenberg, Santosh Nagarakatte, Peter-Michael
Osera, Milo M. K. Martin, and Steve Zdancewic.
Ironclad C++: A Library-Augmented Type-Safe Subset of C++.
In Proceedings of the 28th Annual ACM SIGPLAN Conference on
Object-Oriented Programming, Systems, Languages, and Applications, (OOPSLA),
2013.
[ PDF
Abstract ]
|
[32]
|
Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic.
Watchdog: Hardware for Safe and Secure Manual Memory Management
and Full Memory Safety.
In Proceedings of the 39th International Symposium on Computer
Architecture (ISCA), June 2012.
[ PDF
Abstract ]
|
[33]
|
Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic.
Formalizing the LLVM Intermediate Representation for Verified
Program Transformations.
In Proc. of the ACM Symposium on Principles of Programming
Languages (POPL), 2012.
[ PDF
Abstract ]
|
[34]
|
Jianzhou Zhao and Steve Zdancewic.
Mechanized Verification of Computing Dominators for Formalizing
Compilers.
In The Second International Conference on Certified Programs and
Proofs (CPP), Lecture Notes in Computer Science, pages 27--42, 2012.
[ PDF
Abstract ]
|
[35]
|
Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve
Zdancewic.
Generative Type Abstraction and Type-level Computation.
In Proc. of the ACM Symposium on Principles of Programming
Languages (POPL), 2011.
[ PDF
Abstract ]
|
[36]
|
Karl Mazurak and Steve Zdancewic.
Lolliproc: to Concurrency from Classical Linear Logic via
Curry-Howard and Control.
In Proc. of the 15th ACM SIGPLAN International Conference on
Functional Programming (ICFP), 2010.
[ PDF
Abstract ]
|
[37]
|
Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, and Steve Zdancewic.
CETS: Compiler-Enforced Temporal Safety for C.
In Proceedings of the ACM International Symposium on Memory
Management (ISMM), 2010.
[ PDF
Abstract ]
|
[38]
|
Jianzhou Zhao, Qi Zhang, and Steve Zdancewic.
Relational Parametricity for Polymorphic Linear Lambda
Calculus.
In Proceedings of the Eighth ASIAN Symposium on Programming
Languages and Systems (APLAS), 2010.
[ PDF
Abstract ]
|
[39]
|
Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, and Steve Zdancewic.
SoftBound: Highly Compatible and Complete Spatial Memory
Safety for C.
In Proc. 2009 ACM SIGPLAN Conference on Programming Languages
Design and Implementation (PLDI), 2009.
[ PDF
Abstract ]
|
[40]
|
J. Nathan Foster, Benjamin C. Pierce, and Steve Zdancewic.
Updatable Security Views.
In Proc. of 22nd IEEE Computer Security Foundations Symposium
(CSF), 2009.
[ PDF
Abstract ]
|
[41]
|
Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjöberg, Stephanie Weirich, and
Steve Zdancewic.
Reactive Noninterference.
In ACM Computer and Communications Security Conference (CCS),
2009.
[ PDF
Abstract ]
|
[42]
|
Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph
Schorr, and Steve Zdancewic.
AURA: A Programming Language for Authorization and Audit.
In Proc. of the 13th ACM SIGPLAN International Conference on
Functional Programming (ICFP), Victoria, British Columbia, Canada, September
2008.
[ PDF
Abstract ]
|
[43]
|
Joe Devietti, Colin Blundell, Milo M.K. Martin, and Steve Zdancewic.
HardBound: Architectural Support for Spatial Safety of the C
Programming Language.
In International Conference on Architectural Support for
Programming Languages and Operating Systems (ASPLOS), March 2008.
[ PDF
Abstract ]
|
[44]
|
Jeffrey A. Vaughan, Limin Jia, Karl Mazurak, and Steve Zdancewic.
Evidence-based Audit.
In Proc. of 21st IEEE Computer Security Foundations Symposium
(CSF), pages 177--191. IEEE Computer Society Press, 2008.
[ PDF
Abstract ]
|
[45]
|
Peng Li and Steve Zdancewic.
Combining Events And Threads For Scalable Network Services.
In Proc. 2007 ACM SIGPLAN Conference on Programming Languages
Design and Implementation (PLDI), pages 189--199, 2007.
[ PS
Abstract ]
|
[46]
|
Jeffrey A. Vaughan and Steve Zdancewic.
A Cryptographic Decentralized Label Model.
In IEEE 2007 Symposium on Security and Privacy (Oakland),
pages 192--206, 2007.
[ PDF
PS
Abstract ]
|
[47]
|
Nikhil Swamy, Michael Hicks, Stephen Tse, and Steve Zdancewic.
Managing Policy Updates in Security-Typed Languages.
In Proc. of 19th IEEE Computer Security Foundations Workshop
(CSFW), pages 202--216. IEEE Computer Society Press, 2006.
[ PDF
Abstract ]
|
[48]
|
Peng Li and Steve Zdancewic.
Encoding Information Flow in Haskell.
In Proc. of 19th IEEE Computer Security Foundations Workshop
(CSFW), pages 16--27. IEEE Computer Society Press, 2006.
[ PDF
Abstract ]
|
[49]
|
Rajeev Alur, Pavol Černý, and Steve Zdancewic.
Preserving Secrecy under Refinement.
In Proc. of 33rd International Colloquium on Automata, Languages
and Programming (ICALP), pages 107--118, 2006.
[ PDF
Abstract ]
|
[50]
|
Peng Li and Steve Zdancewic.
Downgrading Policies and Relaxed Noninterference.
In Proc. 32nd ACM Symp. on Principles of Programming Languages
(POPL), pages 158--170, January 2005.
[ PDF
Abstract ]
|
[51]
|
Peng Li and Steve Zdancewic.
Practical Information-flow Control in Web-based Information
Systems.
In Proc. of 18th IEEE Computer Security Foundations Workshop
(CSFW), pages 2--15, 2005.
[ PDF
Abstract ]
|
[52]
|
Stephen Tse and Steve Zdancewic.
Designing a Security-typed Language with Certificate-based
Declassification.
In Proc. of the 14th European Symposium on Programming (ESOP),
volume 3444, pages 279--294, 2005.
[ PDF
Abstract ]
|
[53]
|
Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster,
Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn,
Stephanie Weirich, and Steve Zdancewic.
Mechanized Metatheory for the Masses: The POPLMark Challenge.
In International Conference on Theorem Proving in Higher Order
Logics (TPHOLs), pages 50--65, 2005.
[ PDF
Abstract ]
|
[54]
|
Peng Li and Steve Zdancewic.
Advanced Control Flow in Java Card Programming.
In Proceedings of the 2004 ACM SIGPLAN/SIGBED Conference on
Languages, Compilers, and Tools for Embedded Systems (LCTES), pages
165--174, June 2004.
[ PDF
Abstract ]
|
[55]
|
Stephen Tse and Steve Zdancewic.
Run-time Principals in Information-flow Type Systems.
In IEEE 2004 Symposium on Security and Privacy (Oakland), pages
179--193. IEEE Computer Society Press, May 2004.
[ PDF
PS
Abstract ]
|
[56]
|
Stephen Tse and Steve Zdancewic.
Translating Dependency into Parametricity.
In Proc. of the 9th ACM SIGPLAN International Conference on
Functional Programming (ICFP), 2004.
[ PDF
PS
Abstract ]
|
[57]
|
Andrew C. Myers, Andrei Sabelfeld, and Steve Zdancewic.
Enforcing Robust Declassification.
In Proc. of 17th IEEE Computer Security Foundations Workshop
(CSFW), pages 172--186, 2004.
[ PDF
Abstract ]
|
[58]
|
David Walker, Steve Zdancewic, and Jay Ligatti.
A Theory of Aspects.
In Proc. of the 8th ACM SIGPLAN International Conference on
Functional Programming (ICFP), pages 127--139, Upsala, Sweden, August 2003.
[ PDF
PS
Abstract ]
|
[59]
|
Steve Zdancewic and Andrew C. Myers.
Observational Determinism for Concurrent Program Security.
In Proc. of 16th IEEE Computer Security Foundations Workshop
(CSFW), pages 29--45, Asilomar, CA, July 2003.
[ PDF
PS
Abstract ]
|
[60]
|
Lantian Zheng, Stephen Chong, Steve Zdancewic, and Andrew C. Myers.
Building Secure Distributed Systems Using Replication and
Partitioning.
In IEEE 2003 Symposium on Security and Privacy (Oakland),
pages 236--250. IEEE Computer Society Press, 2003.
[ PDF
PS
Abstract ]
|
[61]
|
Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, and Andrew C. Myers.
Untrusted Hosts and Confidentiality: Secure Program
Partitioning.
In Proc. 18th ACM Symp. on Operating System Principles
(SOSP), volume 35(5) of Operating Systems Review, pages 1--14, Banff,
Canada, October 2001.
[ PDF
PS
Abstract ]
|
[62]
|
Steve Zdancewic and Andrew C. Myers.
Robust Declassification.
In Proc. of 14th IEEE Computer Security Foundations Workshop
(CSFW), pages 15--23, Cape Breton, Canada, June 2001.
[ PDF
PS
Abstract ]
|
[63]
|
Steve Zdancewic and Andrew C. Myers.
Secure Information Flow and CPS.
In Proc. of the 10th European Symposium on Programming (ESOP),
volume 2028 of Lecture Notes in Computer Science, pages 46--61, April
2001.
[ PDF
PS
Abstract ]
|
[64]
|
Steve Zdancewic, Dan Grossman, and Greg Morrisett.
Principals in Programming Languages: A Syntactic Proof
Technique.
In Proc. of the 4th ACM SIGPLAN International Conference on
Functional Programming (ICFP), pages 197--207, Paris, France, September
1999.
[ PDF
PS
Abstract ]
|
|
Workshop Papers
[1]
|
Neelakantan R. Krishnaswami, Jennifer Paykin, and Steve Zdancewic.
Curry-Howard for GUIs.
In POPL Off the Beaten Track (OBT), 2015.
[ PDF ]
|
[2]
|
Jennifer Paykin and Steve Zdancewic.
A Linear/Producer/Consumer model of Classical Linear Logic
(extended abstract).
In Third International Workshop on Linearity, LINEARITY, 2014.
[ PDF
Abstract ]
|
[3]
|
Peter-Michael Osera, Vilhelm Sjöberg, and Steve Zdancewic.
Dependent Ineroperability.
In The Sixth ACM SIGPLAN Workshop on Programming Languages meets
Program Verification (PLPV), 2012.
[ PDF
Abstract ]
|
[4]
|
Karl Mazurak, Jianzhou Zhao, and Steve Zdancewic.
Lightweight linear types in System Fo.
In ACM SIGPLAN International Workshop on Types in Languages
Design and Implementation (TLDI), pages 77--88, 2010.
[ PDF
Abstract ]
|
[5]
|
Limin Jia and Steve Zdancewic.
Encoding information flow in Aura.
In Proceedings of the 2009 Workshop on Programming Languages and
Analysis for Security (PLAS), pages 17--29, 2009.
[ PDF
Abstract ]
|
[6]
|
Michael J. May, Carl A. Gunter, Insup Lee, and Steve Zdancewic.
Strong and Weak Policy Relations.
In POLICY 2009, IEEE International Symposium on Policies for
Distributed Systems and Networks, pages 33--36, 2009.
|
[7]
|
Karl Mazurak and Steve Zdancewic.
ABash: Finding Bugs in Bash Scripts.
In ACM SIGPLAN Workshop on Programming Languages and Analysis
for Security (PLAS), June 2007.
[ PDF
Abstract ]
|
[8]
|
Peng Li and Steve Zdancewic.
Unifying Confidentiality and Integrity in Downgrading
Policies.
In Proc. of Foundations of Computer Security Workshop (FCS),
2005.
[ PDF
Abstract ]
|
[9]
|
Michael Hicks, Stephen Tse, Boniface Hicks, and Steve Zdancewic.
Dynamic updating of information-flow policies.
In Proc. of Foundations of Computer Security Workshop (FCS),
2005.
[ PDF
Abstract ]
|
[10]
|
Peng Li, Yun Mao, and Steve Zdancewic.
Information Integrity Policies.
In Proceedings of the Workshop on Formal Aspects in Security &
Trust (FAST), September 2003.
[ PDF
PS
Abstract ]
|
[11]
|
Usa Sammapun, Raman Sharykin, Margaret Delap, Myong Kim, and Steve Zdancewic.
Formalizing Java-MaC.
In Proceedings of the Third Runtime Verification Workshop,
pages 171--190. Electronic Notes in Theoretical Computer Science, July 2003.
[ PDF
PS
Abstract ]
|
[12]
|
Michael Greenwald, Carl A. Gunter, Björn Knutsson, Andre Scedrov,
Jonathan M. Smith, and Steve Zdancewic.
Computer Security is Not a Science (but it should be).
In Proceedings of the Large-Scale Network Security Workshop,
March 2003.
[ PDF
PS ]
|
[13]
|
Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick
Smith, David Walker, Stephanie Weirich, and Steve Zdancewic.
TALx86: A Realistic Typed Assembly Language.
In 2nd ACM SIGPLAN Workshop on Compiler Support for System
Software, pages 25--35, 1999.
[ PDF
PS
Abstract ]
|
|
Edited Volumes
[1]
|
Pierpaolo Degano, Ralf Küsters, Luca Viganò, and Steve Zdancewic,
editors.
Joint workshop on foundations of computer security and automated
reasoning for security protocol analysis (FCS-ARSPA '06), volume 206 of
Information and Computation.
Elsevier, 2008.
|
[2]
|
Vugranam C. Shreedhar and Steve Zdancewic, editors.
Proceedings of the 2006 Workshop on Programming Languages and
Analysis for Security (PLAS).
ACM, 2006.
|
|
Technical Reports, Work in Progress, and Unpublished Papers
[1]
|
Jennifer Paykin and Steve Zdancewic.
A HoTT Quantum Equational Theory (Extended Version).
available on arXiv, 2019.
[ http
Abstract ]
|
[2]
|
Dmitri Garbuzov, William Mansky, Christine Rizkallah, and Steve Zdancewic.
Structural Operational Semantics for Control Flow Graph
Machines, 2018.
[ arXiv
PDF
Abstract ]
|
[3]
|
Jennifer Paykin and Steve Zdancewic.
A Linear/Producer/Consumer model of Classical Linear Logic.
Technical report, University of Pennsylvania, 2014.
[ PDF
Abstract ]
|
[4]
|
Christian DeLozier, Richard Eisenberg, Santosh Nagarakatte, Peter-Michael
Osera, Milo M.K. Martin, and Steve Zdancewic.
Ironclad C++: A library-Augmented Type-Safe Subset of C++.
Technical Report MS-CIS-13-05, University of Pennsylvania, March
2013.
[ PDF ]
|
[5]
|
Jianzhou Zhao, Qi Zhang, and Steve Zdancewic.
Relational Parametricity for Polymorphic Linear Lambda Calculus
(Extended TR).
2010.
[ PDF
Abstract ]
|
[6]
|
Jeffrey C. Vaughan, Limin Jia, Karl Mazurak, and Steve Zdancewic.
Evidence-based Audit, Technical Appendix.
Technical Report MS-CIS-08-09, University of Pennsylvania, 2008.
[ PDF ]
|
[7]
|
Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph
Schorr, and Steve Zdancewic.
AURA:Preliminary Technical Results.
Technical Report MS-CIS-08-10, University of Pennsylvania, 2008.
[ PDF ]
|
[8]
|
Stephen Tse and Steve Zdancewic.
Concise Concrete Syntax.
Technical Report MS-CIS-08-11, University of Pennsylvania, 2008.
[ PDF ]
|
[9]
|
Brian Aydemir, Stephanie Weirich, and Steve Zdancewic.
Abstracting Syntax.
(15 pages), 2008.
|
[10]
|
Stephen Tse and Steve Zdancewic.
Translating Dependency into Parametricity.
(33 pages) Accepted to Journal of Functional Programming,
pending revisions, 2006.
|
[11]
|
Stephen Tse and Steve Zdancewic.
Translating Dependency into Parametricity.
Technical Report MIS-CIS-04-01, University of Pennsylvania, 2004.
[ PDF
Abstract ]
|
[12]
|
Stephen Tse and Steve Zdancewic.
Designing a Security-typed Language with Certificate-based
Declassification.
Technical Report MIS-CIS-04-16, University of Pennsylvania, 2004.
[ PDF
Abstract ]
|
[13]
|
Stephen Tse and Steve Zdancewic.
Run-time Principals in Information-flow Type Systems.
Technical Report MS-CIS-03-39, University of Pennsylvania, 2003.
The conference version appears in IEEE Security and Privacy 2004.
[ PDF
PS
Abstract ]
|
[14]
|
Stephan A. Zdancewic.
Programming Languages for Information Security.
PhD thesis, Cornell University, August 2002.
[ PDF
PS
Abstract ]
|
[15]
|
Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, and Andrew C. Myers.
Secure Program Partitioning.
Technical Report 2001-1846, Computer Science Dept., Cornell
University, 2001.
[ PDF
PS
Abstract ]
|
[16]
|
Steve Zdancewic and Andrew C. Myers.
Confidentiality and Integrity with Untrusted Hosts.
Technical Report 2000-1810, Computer Science Dept., Cornell
University, 2000.
[ PDF
PS
Abstract ]
|
[17]
|
Steve Zdancewic and Dan Grossman.
Principals in Programming Languages: Technical Results.
Technical Report TR99-1752, Computer Science Dept., Cornell
University, June 1999.
[ PDF
PS
Abstract ]
|
|
Copyright Information
The documents contained in these directories are included by the
contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a non-commercial basis. Copyright and
all rights therein are maintained by the authors or by other copyright
holders, notwithstanding that they have offered their works here
electronically. It is understood that all persons copying this
information will adhere to the terms and constraints invoked by each
author's copyright. These works may not be reposted without the
explicit permission of the copyright holder.
|
Parts of this page were generated by
bibtex2html
|
Last modified:
Mon Apr 29 11:24:13 EDT 2024
| |