default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDSteve Zdancewic
Person information
- affiliation: University of Pennsylvania, Philadelphia, PA, USA
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[j28]Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski, Steve Zdancewic:
A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer-Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction. Proc. ACM Program. Lang. 8(ICFP): 789-817 (2024)- [j27]Stephen Mell
, Steve Zdancewic, Osbert Bastani:
Optimal Program Synthesis via Abstract Interpretation. Proc. ACM Program. Lang. 8(POPL): 457-481 (2024) - [i14]Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski, Steve Zdancewic:
A Two-Phase Infinite/Finite Low-Level Memory Model. CoRR abs/2404.16143 (2024) - [i13]Stephen Mell, Steve Zdancewic, Osbert Bastani:
An Opportunistically Parallel Lambda Calculus for Performant Composition of Large Language Models. CoRR abs/2405.11361 (2024) - [i12]Eleftherios Ioannidis, Yannick Zakowski, Steve Zdancewic, Sebastian Angel:
Structural temporal logic for mechanized program verification. CoRR abs/2410.14906 (2024) - 2023
- [j26]Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, Steve Zdancewic:
Semantics for Noninterference with Interaction Trees (Artifact). Dagstuhl Artifacts Ser. 9(2): 06:1-06:2 (2023) - [j25]Nick Rioux, Xuejing Huang, Bruno C. d. S. Oliveira, Steve Zdancewic:
A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈. Proc. ACM Program. Lang. 7(POPL): 515-543 (2023) - [j24]Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic:
Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq. Proc. ACM Program. Lang. 7(POPL): 1770-1800 (2023) - [c71]Stephen Mell, Favyen Bastani, Steve Zdancewic, Osbert Bastani:
Synthesizing Trajectory Queries from Examples. CAV (1) 2023: 459-484 - [c70]Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, Steve Zdancewic:
Semantics for Noninterference with Interaction Trees. ECOOP 2023: 29:1-29:29 - [c69]Lawrence Dunn, Val Tannen, Steve Zdancewic:
Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure. ITP 2023: 14:1-14:20 - [c68]Lawrence Dunn, Val Tannen, Steve Zdancewic:
Syntax Monads for the Working Formal Metatheorist. ACT 2023: 98-117 - [e3]Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic:
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023. ACM 2023 [contents] - 2022
- [j23]Irene Yoon, Yannick Zakowski, Steve Zdancewic:
Formal reasoning about layered monadic interpreters. Proc. ACM Program. Lang. 6(ICFP): 254-282 (2022) - [j22]Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, Steve Zdancewic:
C4: verified transactional objects. Proc. ACM Program. Lang. 6(OOPSLA1): 1-31 (2022) - [c67]George Tolkachev, Stephen Mell, Steve Zdancewic, Osbert Bastani:
Counterfactual Explanations for Natural Language Interfaces. ACL (2) 2022: 113-118 - [c66]Stephen Mell, Osbert Bastani, Steve Zdancewic:
Ideograph: A Language for Expressing and Manipulating Structured Data. TERMGRAPH@FSCD 2022: 65-84 - [e2]Andrei Popescu, Steve Zdancewic:
CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022. ACM 2022, ISBN 978-1-4503-9182-5 [contents] - [i11]George Tolkachev, Stephen Mell, Steve Zdancewic, Osbert Bastani:
Counterfactual Explanations for Natural Language Interfaces. CoRR abs/2204.13192 (2022) - [i10]Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic:
Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq. CoRR abs/2211.06863 (2022) - 2021
- [j21]Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, Steve Zdancewic:
Modular, compositional, and executable formal semantics for LLVM IR. Proc. ACM Program. Lang. 5(ICFP): 1-30 (2021) - [j20]Paul He, Eddy Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl Smeltzer, Andrei Stefanescu, Aaron Tomb, Adam Wick, Matthew Yacavone, Steve Zdancewic:
A type system for extracting functional specifications from memory-safe imperative programs. Proc. ACM Program. Lang. 5(OOPSLA): 1-29 (2021) - [j19]Lucas Silver, Steve Zdancewic:
Dijkstra monads forever: termination-sensitive specifications for interaction trees. Proc. ACM Program. Lang. 5(POPL): 1-28 (2021) - [c65]Yishuai Li, Benjamin C. Pierce, Steve Zdancewic:
Model-based testing of networked applications. ISSTA 2021: 529-539 - [c64]Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, Steve Zdancewic:
Verifying an HTTP Key-Value Server with Interaction Trees and VST. ITP 2021: 32:1-32:19 - [d1]Yishuai Li, Benjamin C. Pierce, Steve Zdancewic:
Replication Package for Article: Model-Based Testing of Networked Applications. Zenodo, 2021
- [i9]Yishuai Li, Benjamin C. Pierce, Steve Zdancewic:
Model-Based Testing of Networked Applications. CoRR abs/2102.00378 (2021) - 2020
- [j18]Nick Rioux, Steve Zdancewic:
Computation focusing. Proc. ACM Program. Lang. 4(ICFP): 95:1-95:27 (2020) - [j17]Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic:
Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang. 4(POPL): 51:1-51:32 (2020) - [c63]Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic:
An equational theory for weak bisimulation via generalized parameterized coinduction. CPP 2020: 71-84 - [i8]Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic:
An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction. CoRR abs/2001.02659 (2020)
2010 – 2019
- 2019
- [j16]Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic:
Synthesizing symmetric lenses. Proc. ACM Program. Lang. 3(ICFP): 95:1-95:28 (2019) - [c62]Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic:
From C to interaction trees: specifying, verifying, and testing a networked server. CPP 2019: 234-248 - [c61]Marcella Hastings, Brett Hemenway, Daniel Noble, Steve Zdancewic:
SoK: General Purpose Compilers for Secure Multi-Party Computation. IEEE Symposium on Security and Privacy 2019: 1220-1237 - [i7]Jennifer Paykin, Steve Zdancewic:
A HoTT Quantum Equational Theory (Extended Version). CoRR abs/1904.04371 (2019) - [i6]Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic:
Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress). CoRR abs/1906.00046 (2019) - 2018
- [j15]Steve Zdancewic:
Technical perspective: Building bug-free compilers. Commun. ACM 61(2): 83 (2018) - [j14]Jennifer Paykin, Steve Zdancewic:
A linear/producer/consumer model of classical linear logic. Math. Struct. Comput. Sci. 28(5): 710-735 (2018) - [j13]Solomon Maina, Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic:
Synthesizing quotient lenses. Proc. ACM Program. Lang. 2(ICFP): 80:1-80:29 (2018) - [j12]Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic:
Synthesizing bijective lenses. Proc. ACM Program. Lang. 2(POPL): 1:1-1:30 (2018) - [c60]Christine Rizkallah, Dmitri Garbuzov, Steve Zdancewic:
A Formal Equational Theory for Call-By-Push-Value. ITP 2018: 523-541 - [c59]Robert Rand, Jennifer Paykin, Dong-Ho Lee, Steve Zdancewic:
ReQWIRE: Reasoning about Reversible Quantum Circuits. QPL 2018: 299-312 - [i5]Dmitri Garbuzov, William Mansky, Christine Rizkallah, Steve Zdancewic:
Structural Operational Semantics for Control Flow Graph Machines. CoRR abs/1805.05400 (2018) - [i4]Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic:
Synthesizing Symmetric Lenses. CoRR abs/1810.11527 (2018) - [i3]Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic:
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server. CoRR abs/1811.11911 (2018) - 2017
- [c58]William Mansky, Yuanfeng Peng, Steve Zdancewic, Joseph Devietti:
Verifying dynamic race detection. CPP 2017: 151-163 - [c57]Jennifer Paykin, Steve Zdancewic:
The linearity Monad. Haskell 2017: 117-132 - [c56]Jennifer Paykin, Robert Rand, Steve Zdancewic:
QWIRE: a core language for quantum circuits. POPL 2017: 846-858 - [c55]Robert Rand, Jennifer Paykin, Steve Zdancewic:
QWIRE Practice: Formal Verification of Quantum Circuits in Coq. QPL 2017: 119-132 - [i2]Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic:
Synthesizing Bijective Lenses. CoRR abs/1710.03248 (2017) - 2016
- [c54]Jennifer Paykin, Steve Zdancewic:
Linear λμ is CP (more or less). A List of Successes That Can Change the World 2016: 273-291 - [c53]Jonathan Frankle, Peter-Michael Osera, David Walker, Steve Zdancewic:
Example-directed synthesis: a type-theoretic interpretation. POPL 2016: 802-815 - 2015
- [c52]William Mansky, Dmitri Garbuzov, Steve Zdancewic:
An Axiomatic Specification for Sequential Memory Models. CAV (2) 2015: 413-428 - [c51]Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis:
A formal C memory model supporting integer-pointer casts. PLDI 2015: 326-335 - [c50]Peter-Michael Osera, Steve Zdancewic:
Type-and-example-directed program synthesis. PLDI 2015: 619-630 - [c49]Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic:
Everything You Want to Know About Pointer-Based Checking. SNAPL 2015: 190-208 - [c48]Robert Rand, Steve Zdancewic:
VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs. MFPS 2015: 351-367 - 2014
- [j11]Benoît Valiron, Steve Zdancewic:
Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector Spaces. Sci. Ann. Comput. Sci. 24(2): 325-368 (2014) - [c47]Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic:
WatchdogLite: Hardware-Accelerated Compiler-Based Pointer Checking. CGO 2014: 175 - [c46]Aloïs Brunel, Marco Gaboardi, Damiano Mazza, Steve Zdancewic:
A Core Quantitative Coeffect Calculus. ESOP 2014: 351-370 - [c45]Benoît Valiron, Steve Zdancewic:
Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi. ICTAC 2014: 442-459 - [c44]Jennifer Paykin, Steve Zdancewic:
A Linear/Producer/Consumer Model of Classical Linear Logic. LINEARITY 2014: 9-23 - [i1]Benoît Valiron, Steve Zdancewic:
Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi. CoRR abs/1406.1310 (2014) - 2013
- [j10]Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic:
Hardware-Enforced Comprehensive Memory Safety. IEEE Micro 33(3): 38-47 (2013) - [c43]Christian DeLozier, Richard A. Eisenberg, Santosh Nagarakatte, Peter-Michael Osera, Milo M. K. Martin, Steve Zdancewic:
Ironclad C++: a library-augmented type-safe subset of c++. OOPSLA 2013: 287-304 - [c42]Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic:
Formal verification of SSA-based optimizations for LLVM. PLDI 2013: 175-186 - 2012
- [c41]Jianzhou Zhao, Steve Zdancewic:
Mechanized Verification of Computing Dominators for Formalizing Compilers. CPP 2012: 27-42 - [c40]Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic:
Watchdog: Hardware for safe and secure manual memory management and full memory safety. ISCA 2012: 189-200 - [c39]Peter-Michael Osera, Vilhelm Sjöberg, Steve Zdancewic:
Dependent interoperability. PLPV 2012: 3-14 - [c38]Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic:
Formalizing the LLVM intermediate representation for verified program transformations. POPL 2012: 427-440 - 2011
- [c37]Stephanie Weirich, Dimitrios Vytiniotis, Simon L. Peyton Jones, Steve Zdancewic:
Generative type abstraction and type-level computation. POPL 2011: 227-240 - 2010
- [j9]Peng Li, Steve Zdancewic:
Arrows for secure information flow. Theor. Comput. Sci. 411(19): 1974-1994 (2010) - [c36]Jianzhou Zhao, Qi Zhang, Steve Zdancewic:
Relational Parametricity for a Polymorphic Linear Lambda Calculus. APLAS 2010: 344-359 - [c35]Karl Mazurak, Steve Zdancewic:
Lolliproc: to concurrency from classical linear logic via curry-howard and control. ICFP 2010: 39-50 - [c34]Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, Steve Zdancewic:
CETS: compiler enforced temporal safety for C. ISMM 2010: 31-40 - [c33]Karl Mazurak, Jianzhou Zhao, Steve Zdancewic:
Lightweight linear types in system fdegree. TLDI 2010: 77-88
2000 – 2009
- 2009
- [j8]Jim Allen, Zena M. Ariola, Pierre-Louis Curien, Matthew Fluet, Jeffrey S. Foster, Dan Grossman, Robert Harper, Hugo Herbelin, Yannis Smaragdakis, David Walker, Steve Zdancewic:
An overview of the Oregon programming languages summer school. ACM SIGPLAN Notices 44(11): 1-3 (2009) - [c32]Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjöberg, Stephanie Weirich, Steve Zdancewic:
Reactive noninterference. CCS 2009: 79-90 - [c31]J. Nathan Foster, Benjamin C. Pierce, Steve Zdancewic:
Updatable Security Views. CSF 2009: 60-74 - [c30]Limin Jia, Steve Zdancewic:
Encoding information flow in Aura. PLAS 2009: 17-29 - [c29]Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, Steve Zdancewic:
SoftBound: highly compatible and complete spatial memory safety for c. PLDI 2009: 245-258 - [c28]Michael J. May, Carl A. Gunter, Insup Lee, Steve Zdancewic:
Strong and Weak Policy Relations. POLICY 2009: 33-36 - 2008
- [j7]Pierpaolo Degano, Ralf Küsters, Luca Viganò, Steve Zdancewic:
Joint workshop on foundations of computer security and automated reasoning for security protocol analysis (FCS-ARSPA '06). Inf. Comput. 206(2-4): 129 (2008) - [c27]Joe Devietti, Colin Blundell, Milo M. K. Martin, Steve Zdancewic:
Hardbound: architectural support for spatial safety of the C programming language. ASPLOS 2008: 103-114 - [c26]Jeffrey A. Vaughan, Limin Jia, Karl Mazurak, Steve Zdancewic:
Evidence-Based Audit. CSF 2008: 177-191 - [c25]Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr, Steve Zdancewic:
AURA: a programming language for authorization and audit. ICFP 2008: 27-38 - 2007
- [j6]Stephen Tse, Steve Zdancewic:
Run-time principals in information-flow type systems. ACM Trans. Program. Lang. Syst. 30(1): 6 (2007) - [c24]Peng Li, Steve Zdancewic:
Combining events and threads for scalable network services implementation and evaluation of monadic, application-level concurrency primitives. PLDI 2007: 189-199 - [c23]Steve Zdancewic:
Application-level concurrency: combining events and treads: invited talk. DAMP 2007: 2 - [c22]Jeffrey A. Vaughan, Steve Zdancewic:
A Cryptographic Decentralized Label Model. S&P 2007: 192-206 - 2006
- [j5]Andrew C. Myers, Andrei Sabelfeld, Steve Zdancewic:
Enforcing Robust Declassification and Qualified Robustness. J. Comput. Secur. 14(2): 157-196 (2006) - [j4]Jay Ligatti, David Walker, Steve Zdancewic:
A type-theoretic interpretation of pointcuts and advice. Sci. Comput. Program. 63(3): 240-266 (2006) - [c21]Peng Li, Steve Zdancewic:
Encoding Information Flow in Haskell. CSFW 2006: 16 - [c20]Nikhil Swamy, Michael Hicks, Stephen Tse, Steve Zdancewic:
Managing Policy Updates in Security-Typed Languages. CSFW 2006: 202-216 - [c19]Rajeev Alur, Pavol Cerný, Steve Zdancewic:
Preserving Secrecy Under Refinement. ICALP (2) 2006: 107-118 - [e1]Vugranam C. Sreedhar, Steve Zdancewic:
Proceedings of the 2006 Workshop on Programming Languages and Analysis for Security, PLAS 2006, Ottawa, Ontario, Canada, June 10, 2006. ACM 2006, ISBN 1-59593-374-3 [contents] - 2005
- [c18]Peng Li, Steve Zdancewic:
Practical Information-flow Control in Web-Based Information Systems. CSFW 2005: 2-15 - [c17]Stephen Tse, Steve Zdancewic:
A Design for a Security-Typed Language with Certificate-Based Declassification. ESOP 2005: 279-294 - [c16]Peng Li, Steve Zdancewic:
Downgrading policies and relaxed noninterference. POPL 2005: 158-170 - [c15]Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, Steve Zdancewic:
Mechanized Metatheory for the Masses: The PoplMark Challenge. TPHOLs 2005: 50-65 - [c14]Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, Steve Zdancewic:
It Is Time to Mechanize Programming Language Metatheory. VSTTE 2005: 26-30 - 2004
- [c13]Andrew C. Myers, Andrei Sabelfeld, Steve Zdancewic:
Enforcing Robust Declassification. CSFW 2004: 172-186 - [c12]Stephen Tse, Steve Zdancewic:
Translating dependency into parametricity. ICFP 2004: 115-125 - [c11]Peng Li, Steve Zdancewic:
Advanced control flow in Java card programming. LCTES 2004: 165-174 - [c10]Stephen Tse, Steve Zdancewic:
Run-time Principals in Information-flow Type Systems. S&P 2004: 179-193 - 2003
- [c9]Steve Zdancewic, Andrew C. Myers:
Observational Determinism for Concurrent Program Security. CSFW 2003: 29- - [c8]David Walker, Steve Zdancewic, Jay Ligatti:
A theory of aspects. ICFP 2003: 127-139 - [c7]Steve Zdancewic:
A Type System for Robust Declassification. MFPS 2003: 263-277 - [c6]Lantian Zheng, Stephen Chong, Andrew C. Myers, Steve Zdancewic:
Using Replication and Partitioning to Build Secure Distributed Systems. S&P 2003: 236-250 - [c5]Usa Sammapun, Raman Sharykin, Margaret DeLap, Myong Kim, Steve Zdancewic:
Formalizing Java-MaC. RV@CAV 2003: 171-190 - 2002
- [b1]Steve Zdancewic:
Programming Languages for Information Security. Cornell University, USA, 2002 - [j3]Steve Zdancewic, Andrew C. Myers:
Secure Information Flow via Linear Continuations. High. Order Symb. Comput. 15(2-3): 209-234 (2002) - [j2]Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, Andrew C. Myers:
Secure program partitioning. ACM Trans. Comput. Syst. 20(3): 283-328 (2002) - 2001
- [c4]Steve Zdancewic, Andrew C. Myers:
Robust Declassification. CSFW 2001: 15-23 - [c3]Steve Zdancewic, Andrew C. Myers:
Secure Information Flow and CPS. ESOP 2001: 46-61 - [c2]Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, Andrew C. Myers:
Untrusted Hosts and Confidentiality: Secure Program Partitioning. SOSP 2001: 1-14 - 2000
- [j1]Dan Grossman, J. Gregory Morrisett, Steve Zdancewic:
Syntactic type abstraction. ACM Trans. Program. Lang. Syst. 22(6): 1037-1080 (2000)
1990 – 1999
- 1999
- [c1]