BibSLEIGH — Zhong

Travelled to:

1 × Austria
1 × Cyprus
1 × Denmark
1 × Estonia
1 × France
1 × India
1 × Japan
1 × Portugal
14 × USA
2 × Canada
2 × Poland
2 × The Netherlands
2 × United Kingdom

Collaborated with:

X.Feng V.Trifonov J.Hoffmann A.W.Appel ∅ A.Stampoulis C.League B.Saha R.Gu Z.Ni S.Monnier Q.Carbonneaux D.Yu R.Ferreira David Costanzo A.Vaynberg N.A.Hamid T.Ramananandro X.(.Wu S.Weng Y.Guo V.Sjöberg M.L.0001 L.Rieg H.Liang M.Marmar H.Cai J.H.Reppy Y.Wang P.Wilke Hao Chen 0023 Y.Dong A.McCreight C.Lin L.Li N.Papaspyrou J.H.0002 T.W.Reps Yuyang Sang J.Koenig S.Xiang X.Guo M.Lesourd Joshua Lockerman J.Kim M.Yoon H.Zhang Jieung Kim

Talks about:

certifi (10) type (9) verif (7) code (7) program (6) concurr (6) analysi (6) abstract (5) languag (5) assembl (5)

Person: Zhong Shao

DBLP: Shao:Zhong

Facilitated 2 volumes:

Contributed to:

2015

2014

2013

2012

2010

2008

2007

2006

2005

2004

2003

2002

2001

2000

1999

1998

1997

1995

1994

1993

2017

2019

2016

2018

2019

2020

Wrote 42 papers:

ESOP-2015-0002S #automation #cost analysis #parallel #source code: Automatic Static Cost Analysis for Parallel Programs (JH, ZS), pp. 132–157.
PLDI-2015-Carbonneaux0S #bound #composition: Compositional certified resource bounds (QC, JH, ZS), pp. 467–478.
POPL-2015-GuKRSWWZG #abstraction #specification: Deep Specifications and Certified Abstraction Layers (RG, JK, TR, ZS, X(W, SCW, HZ, YG), pp. 595–608.
FLOPS-2014-HoffmannS #analysis #array #integer #type system: Type-Based Amortized Resource Analysis with Integers and Arrays (JH, ZS), pp. 152–168.
LICS-CSL-2014-LiangFS #composition #concurrent #refinement #source code #verification: Compositional verification of termination-preserving refinement of concurrent programs (HL, XF, ZS), p. 10.
PLDI-2014-Carbonneaux0RS #bound #c #source code #verification: End-to-end verification of stack-space bounds for C programs (QC, JH, TR, ZS), p. 30.
LICS-2013-HoffmannMS #proving #reasoning: Quantitative Reasoning for Proving Lock-Freedom (JH, MM, ZS), pp. 124–133.
POPL-2012-StampoulisS #proving: Static and user-extensible proof checking (AS, ZS), pp. 273–284.
ESOP-2010-FerreiraFS #concurrent #logic #memory management #modelling: Parameterized Memory Models and Concurrent Separation Logic (RF, XF, ZS), pp. 267–286.
ICFP-2010-StampoulisS #logic #named: VeriML: typed computation of logical terms inside a language with effects (AS, ZS), pp. 333–344.
PLDI-2008-FengSDG #hardware #low level #source code #thread: Certifying low-level programs with hardware interrupts and preemptive threads (XF, ZS, YD, YG), pp. 170–182.
ESOP-2007-FengFS #concurrent #logic #on the #reasoning: On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning (XF, RF, ZS), pp. 173–188.
PLDI-2007-CaiSV #self: Certified self-modifying code (HC, ZS, AV), pp. 66–77.
PLDI-2007-McCreightSLL #framework #garbage collection: A general framework for certifying garbage collectors and their mutators (AM, ZS, CL, LL), pp. 468–479.
PLDI-2006-FengSVXN #abstraction #assembly #composition #verification: Modular verification of assembly code with stack-based control abstractions (XF, ZS, AV, SX, ZN), pp. 401–414.
POPL-2006-NiS #assembly #embedded #pointer #programming: Certified assembly programming with embedded code pointers (ZN, ZS), pp. 320–333.
ICFP-2005-FengS #assembly #composition #concurrent #termination #thread #verification: Modular verification of concurrent assembly code with dynamic thread creation and termination (XF, ZS), pp. 254–267.
ICFP-2004-YuS #assembly #concurrent #safety #verification: Verification of safety properties for concurrent assembly code (DY, ZS), pp. 175–188.
CC-2003-LeagueST #compilation #java #precise: Precision in Practice: A Type-Preserving Java Compiler (CL, ZS, VT), pp. 106–120.
ESOP-2003-YuHS #library: Building Certified Libraries for PCC: Dynamic Storage Allocation (DY, NAH, ZS), pp. 363–379.
LICS-2002-HamidSTMN #approach: A Syntactic Approach to Foundational Proof-Carrying Code (NAH, ZS, VT, SM, ZN), pp. 89–100.
POPL-2002-ShaoSTP #type system: A type system for certified binaries (ZS, BS, VT, NP), pp. 217–232.
PLDI-2001-MonnierSS: Principled Scavenging (SM, BS, ZS), pp. 81–91.
ICFP-2000-TrifonovSS #analysis #reflexive: Fully reflexive intensional type analysis (VT, BS, ZS), pp. 82–93.
ESOP-1999-TrifonovS: Safe and Principled Language Interoperation (VT, ZS), pp. 128–146.
ICFP-1999-LeagueST #java #representation: Representing Java Classes in a Typed Intermediate Language (CL, ZS, VT), pp. 183–196.
ICFP-1999-Shao: Transparent Modules with Fully Syntactic Signatures (ZS), pp. 220–232.
ICFP-1998-Shao #compilation: Typed Cross-Module Compilation (ZS), pp. 141–152.
ICFP-1998-ShaoLM #implementation: Implementing Typed Intermediate Languages (ZS, CL, SM), pp. 313–323.
ICFP-1997-Shao #analysis #flexibility #representation: Flexible Representation Analysis (ZS), pp. 85–98.
PLDI-1995-ShaoA #compilation #ml #standard #type system: A Type-Based Compiler for Standard ML (ZS, AWA), pp. 116–129.
LFP-1994-ShaoA: Space-Efficient Closure Representations (ZS, AWA), pp. 150–161.
LFP-1994-ShaoRA: Unrolling Lists (ZS, JHR, AWA), pp. 185–195.
POPL-1993-ShaoA: Smartest Recompilation (ZS, AWA), pp. 439–450.
CAV-2017-Carbonneaux0RS #analysis #automation #coq #proving: Automated Resource Analysis with Coq Proof Objects (QC, JH0, TWR, ZS), pp. 64–85.
CAV-2019-GuoLLRS #analysis #kernel #scheduling: Integrating Formal Schedulability Analysis into a Verified OS Kernel (XG, ML, ML0, LR, ZS), pp. 496–514.
OOPSLA-2019-SjobergSWS #named: DeepSEA: a language for certified system software (VS, YS, SCW, ZS), p. 27.
PLDI-2016-ChenWSLG #composition #kernel #towards #verification: Toward compositional verification of interruptible OS kernels and device drivers (HC0, X(W, ZS, JL, RG), pp. 431–447.
PLDI-2016-CostanzoSG #assembly #c #data flow #security #source code #verification: End-to-end verification of information-flow security for C and assembly programs (DC, ZS, RG), pp. 648–664.
PLDI-2018-GuSKWKS0CR #abstraction #concurrent: Certified concurrent abstraction layers (RG, ZS, JK, X(W, JK, VS, HC0, DC, TR), pp. 646–661.
POPL-2019-WangWS #approach #compilation #composition #stack: An abstract stack based approach to verified compositional compilation to machine code (YW, PW, ZS), p. 30.
POPL-2020-LiuRSGCKY #abstraction #timeline #verification: Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation (ML0, LR, ZS, RG, DC, JEK, MKY), p. 31.