Travelled to:1 × Canada
1 × Russia
10 × USA
Collaborated with:S.K.Lahiri E.Petrank M.Kawaguchi H.Rebêlo J.Yang T.v.Eicken J.Chen B.Parno R.Sinha R.Tate J.Howell J.R.Lorch B.Zill S.Qadeer S.Tasiran K.L.McMillan R.Sharma N.Giannarakis A.Rastogi N.Swamy E.B.Nightingale O.Hodson R.McIlroy G.C.Hunt Aymeric Fromherz A.Narayan D.Zhang F.Perry M.Emmi J.Condit D.Coetzee P.Pratikaki M.Kapritsos M.L.Roberts S.T.V.Setty K.Pawar H.Hashmi S.Gokbulut L.Fernando D.Detlefs S.Wadsworth G.Martínez D.Ahman V.Dumitrescu C.Hritcu M.Narasimhamurthy Z.Paraskevopoulou C.Pit-Claudel J.Protzenko T.Ramananandro
Talks about:autom (6) program (4) system (4) compil (4) languag (3) verif (3) type (3) practic (2) modular (2) assembl (2)
Person: Chris Hawblitzel
DBLP: Hawblitzel:Chris
Contributed to:
20152015
2015
2014
2013
20132012
2010
2009200920082002
20192019Wrote 16 papers:
- CAV-2015-HawblitzelPQT #automation #composition #concurrent #reasoning #refinement #source code
- Automated and Modular Refinement Reasoning for Concurrent Programs (CH, EP, SQ, ST), pp. 449–465.
- CAV-2015-LahiriSH #automation #equivalence
- Automatic Rootcausing for Program Equivalence Failures in Binaries (SKL, RS, CH), pp. 362–379.
- SOSP-2015-HawblitzelHKLPR #distributed #named #proving
- IronFleet: proving practical distributed systems correct (CH, JH, MK, JRL, BP, MLR, STVS, BZ), pp. 1–17.
- OSDI-2014-HawblitzelHLNPZZ #automation #security #verification
- Ironclad Apps: End-to-End Security via Automated Full-System Verification (CH, JH, JRL, AN, BP, DZ, BZ), pp. 165–181.
- CADE-2013-HawblitzelKLR #automation #proving #source code #theorem proving #towards #using
- Towards Modularly Comparing Programs Using Automated Theorem Provers (CH, MK, SKL, HR), pp. 282–299.
- ESEC-FSE-2013-HawblitzelLPHGFDW #compilation #validation
- Will you still compile me tomorrow? static cross-version compiler validation (CH, SKL, KP, HH, SG, LF, DD, SW), pp. 191–201.
- ESEC-FSE-2013-LahiriMSH #difference
- Differential assertion checking (SKL, KLM, RS, CH), pp. 345–355.
- CAV-2012-LahiriHKR #imperative #named #semantics #source code
- SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs (SKL, CH, MK, HR), pp. 712–717.
- PLDI-2010-TateCH #assembly #object-oriented
- Inferable object-oriented typed assembly language (RT, JC, CH), pp. 424–435.
- PLDI-2010-YangH #automation #operating system #type safety #verification
- Safe to the last instruction: automated verification of a type-safe operating system (JY, CH), pp. 99–110.
- POPL-2009-HawblitzelP #automation #garbage collection #verification
- Automated verification of practical garbage collectors (CH, EP), pp. 441–453.
- SOSP-2009-NightingaleHMHH #kernel #multi #named
- Helios: heterogeneous multiprocessing with satellite kernels (EBN, OH, RM, CH, GCH), pp. 221–234.
- PLDI-2008-ChenHPECCP #compilation #object-oriented #optimisation #scalability
- Type-preserving compilation for large-scale optimizing object-oriented compilers (JC, CH, FP, ME, JC, DC, PP), pp. 183–192.
- OSDI-2002-HawblitzelE #flexibility #java #named
- Luna: A Flexible Java Protection System (CH, TvE), pp. 391–401.
- ESOP-2019-MartinezADGHHNP #automation #metaprogramming #proving #smt
- Meta-F* : Proof Automation with SMT, Tactics, and Metaprograms (GM, DA, VD, NG, CH, CH, MN, ZP, CPC, JP, TR, AR, NS), pp. 30–59.
- POPL-2019-FromherzGHPRS #assembly #performance
- A verified, efficient embedding of a verifiable assembly language (AF, NG, CH, BP, AR, NS), p. 30.