Travelled to:1 × Canada
1 × Ireland
1 × United Kingdom
4 × USA
Collaborated with:S.Lerner P.Panchekha M.D.Ernst J.R.Wilcox A.Sanchez-Stern S.Kamil X.Wang S.Kundu I.Sergey D.Woos E.Torlak R.Tate M.Stepp H.Becker E.Darulova M.O.Myreen E.Mullen Daryl Zuniga D.Grossman D.Lazar N.Zeldovich A.Chlipala D.Ricketts V.Robert D.Jang C.Tucker D.Shuffelton R.Jhala Adam T. Geller K.Weitz A.Krishnamurthy T.E.Anderson S.Pernsteiner C.Loncaric X.W.0005 J.Jacky
Talks about:verifi (5) optim (4) system (3) distribut (2) protocol (2) program (2) layout (2) formal (2) compil (2) verif (2)
Person: Zachary Tatlock
DBLP: Tatlock:Zachary
Contributed to:
2015
2014201420102009
2009
2008
2016201920162019201620182018Wrote 16 papers:
- PLDI-2015-PanchekhaSWT #automation #float
- Automatically improving accuracy for floating point expressions (PP, ASS, JRW, ZT), pp. 1–11.
- PLDI-2015-WilcoxWPTWEA #distributed #framework #implementation #named #verification
- Verdi: a framework for implementing and formally verifying distributed systems (JRW, DW, PP, ZT, XW, MDE, TEA), pp. 357–368.
- OSDI-2014-WangLZCT #framework #interpreter #kernel #named
- Jitk: A Trustworthy In-Kernel Interpreter Infrastructure (XW, DL, NZ, AC, ZT), pp. 33–47.
- PLDI-2014-RickettsRJTL #automation #proving
- Automating formal proofs for reactive systems (DR, VR, DJ, ZT, SL), p. 47.
- PLDI-2010-TatlockL #compilation
- Bringing extensibility to verified compilers (ZT, SL), pp. 111–121.
- PLDI-2009-KunduTL #equivalence #optimisation #proving #using
- Proving optimizations correct using parameterized program equivalence (SK, ZT, SL), pp. 327–337.
- POPL-2009-TateSTL #approach #optimisation #similarity
- Equality saturation: a new approach to optimization (RT, MS, ZT, SL), pp. 264–276.
- OOPSLA-2008-TatlockTSJL #refactoring
- Deep typechecking and refactoring (ZT, CT, DS, RJ, SL), pp. 37–52.
- CAV-2016-PernsteinerLTTW #modelling #safety #using
- Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers (SP, CL, ET, ZT, XW0, MDE, JJ), pp. 23–41.
- CAV-2019-BeckerDMT #compilation #named #optimisation
- Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler (HB, ED, MOM, ZT), pp. 155–173.
- OOPSLA-2016-WeitzWTEKT #protocol #scalability #smt #verification
- Scalable verification of border gateway protocol configurations with an SMT solver (KW, DW, ET, MDE, AK, ZT), pp. 765–780.
- OOPSLA-2019-PanchekhaETK #composition #layout #verification #web
- Modular verification of web page layout (PP, MDE, ZT, SK), p. 26.
- PLDI-2016-MullenZTG #optimisation
- Verified peephole optimizations for CompCert (EM, DZ, ZT, DG), pp. 448–461.
- PLDI-2018-PanchekhaGETK #layout #verification #web
- Verifying that web pages have accessible layout (PP, ATG, MDE, ZT, SK), pp. 1–14.
- PLDI-2018-Sanchez-SternPL #fault #float
- Finding root causes of floating point error (ASS, PP, SL, ZT), pp. 256–269.
- POPL-2018-SergeyWT #distributed #programming #protocol #proving
- Programming and proving with distributed protocols (IS, JRW, ZT), p. 30.