Travelled to:1 × Ireland
1 × Sweden
1 × United Kingdom
13 × USA
2 × France
2 × Italy
3 × Canada
Collaborated with:M.M.K.Martin S.Nagarakatte P.Li J.Zhao S.Tse P.Osera J.Paykin D.Walker A.C.Myers K.Mazurak W.Mansky D.Garbuzov B.C.Pierce R.Alur P.Cerný J.Ligatti D.Grossman J.G.Morrisett Robert Rand 0001 C.Hur A.Brunel M.Gaboardi D.Mazza S.Weirich D.Vytiniotis S.L.P.Jones J.Devietti C.Blundell L.Zheng N.Nystrom Jonathan Frankle Anders Miltner K.Fisher J.Kang V.Vafeiadis C.DeLozier R.A.Eisenberg L.Jia J.A.Vaughan L.Zarko J.Schorr L.Xia Yannick Zakowski Paul He G.Malecha
Talks about:program (8) type (6) languag (5) safeti (3) memori (3) formal (3) secur (3) base (3) synthesi (2) support (2)
Person: Steve Zdancewic
DBLP: Zdancewic:Steve
Contributed to:
2015
2015
2014
2014
20132013
20122011
2010
20102009
200820082007
2006200520052004
200420032001
20011999
20172016201720182020Wrote 29 papers:
- CAV-2015-ManskyGZ #axiom #memory management #modelling #specification
- An Axiomatic Specification for Sequential Memory Models (WM, DG, SZ), pp. 413–428.
- PLDI-2015-KangHMGZV #c #memory management
- A formal C memory model supporting integer-pointer casts (JK, CKH, WM, DG, SZ, VV), pp. 326–335.
- PLDI-2015-OseraZ #synthesis
- Type-and-example-directed program synthesis (PMO, SZ), pp. 619–630.
- CGO-2014-NagarakatteMZ #named #pointer
- WatchdogLite: Hardware-Accelerated Compiler-Based Pointer Checking (SN, MMKM, SZ), p. 175.
- ESOP-2014-BrunelGMZ #calculus
- A Core Quantitative Coeffect Calculus (AB, MG, DM, SZ), pp. 351–370.
- OOPSLA-2013-DeLozierENOMZ #c++ #set #type safety
- Ironclad C++: a library-augmented type-safe subset of c++ (CD, RAE, SN, PMO, MMKM, SZ), pp. 287–304.
- PLDI-2013-ZhaoNMZ #optimisation #verification
- Formal verification of SSA-based optimizations for LLVM (JZ, SN, MMKM, SZ), pp. 175–186.
- POPL-2012-ZhaoNMZ #formal method #program transformation #representation
- Formalizing the LLVM intermediate representation for verified program transformations (JZ, SN, MMKM, SZ), pp. 427–440.
- POPL-2011-WeirichVJZ #abstraction #generative
- Generative type abstraction and type-level computation (SW, DV, SLPJ, SZ), pp. 227–240.
- ICFP-2010-MazurakZ #concurrent #linear #logic #named
- Lolliproc: to concurrency from classical linear logic via curry-howard and control (KM, SZ), pp. 39–50.
- ISMM-2010-NagarakatteZMZ #c #compilation #named #safety
- CETS: compiler enforced temporal safety for C (SN, JZ, MMKM, SZ), pp. 31–40.
- PLDI-2009-NagarakatteZMZ #bound #c #memory management #named #safety
- SoftBound: highly compatible and complete spatial memory safety for c (SN, JZ, MMKM, SZ), pp. 245–258.
- ASPLOS-2008-DeviettiBMZ #architecture #bound #c #named #programming language #safety
- Hardbound: architectural support for spatial safety of the C programming language (JD, CB, MMKM, SZ), pp. 103–114.
- ICFP-2008-JiaVMZZSZ #named #programming language
- AURA: a programming language for authorization and audit (LJ, JAV, KM, JZ, LZ, JS, SZ), pp. 27–38.
- PLDI-2007-LiZ #concurrent #evaluation #implementation #monad #network #scalability #thread
- Combining events and threads for scalable network services implementation and evaluation of monadic, application-level concurrency primitives (PL, SZ), pp. 189–199.
- ICALP-v2-2006-AlurCZ #refinement
- Preserving Secrecy Under Refinement (RA, PC, SZ), pp. 107–118.
- ESOP-2005-TseZ #classification #design
- A Design for a Security-Typed Language with Certificate-Based Declassification (ST, SZ), pp. 279–294.
- POPL-2005-LiZ #policy
- Downgrading policies and relaxed noninterference (PL, SZ), pp. 158–170.
- ICFP-2004-TseZ #dependence #parametricity
- Translating dependency into parametricity (ST, SZ), pp. 115–125.
- LCTES-2004-LiZ #control flow #java #programming
- Advanced control flow in Java card programming (PL, SZ), pp. 165–174.
- ICFP-2003-WalkerZL #aspect-oriented #formal method
- A theory of aspects (DW, SZ, JL), pp. 127–139.
- ESOP-2001-ZdancewicM #continuation #data flow
- Secure Information Flow and CPS (SZ, ACM), pp. 46–61.
- SOSP-2001-ZdancewicZNM #clustering
- Untrusted Hosts and Confidentiality: Secure Program Partitioning (SZ, LZ, NN, ACM), pp. 1–14.
- ICFP-1999-ZdancewicGM #programming language #proving
- Principals in Programming Languages: A Syntactic Proof Technique (SZ, DG, JGM), pp. 197–207.
- Haskell-2017-PaykinZ #monad
- The linearity Monad (JP, SZ), pp. 117–132.
- POPL-2016-FrankleOWZ #synthesis
- Example-directed synthesis: a type-theoretic interpretation (JF, PMO, DW, SZ), pp. 802–815.
- POPL-2017-Paykin0Z #named #quantum
- QWIRE: a core language for quantum circuits (JP, RR0, SZ), pp. 846–858.
- POPL-2018-MiltnerFPWZ #lens
- Synthesizing bijective lenses (AM, KF, BCP, DW, SZ), p. 30.
- POPL-2020-XiaZHHMPZ #coq #interactive #recursion #representation #source code
- Interaction trees: representing recursive and impure programs in Coq (LyX, YZ, PH, CKH, GM, BCP, SZ), p. 32.