Zhong Shao

According to our database1, Zhong Shao authored at least 78 papers between 1992 and 2019.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepage:

On csauthors.net:

Bibliography

2019
An abstract stack based approach to verified compositional compilation to machine code.
PACMPL, 2019

A new hierarchical software architecture towards safety-critical aspects of a drone system.
Frontiers of IT & EE, 2019

Integrating Formal Schedulability Analysis into a Verified OS Kernel.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018
Certified concurrent abstraction layers.
Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

2017
Automated Resource Analysis with Coq Proof Objects.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Safety and Liveness of MCS Lock - Layer by Layer.
Proceedings of the Programming Languages and Systems - 15th Asian Symposium, 2017

2016
End-to-end verification of information-flow security for C and assembly programs.
Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

Toward compositional verification of interruptible OS kernels and device drivers.
Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels.
Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation, 2016

2015
Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191).
Dagstuhl Reports, 2015

Deep Specifications and Certified Abstraction Layers.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Compositional certified resource bounds.
Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

Automatic Static Cost Analysis for Parallel Programs.
Proceedings of the Programming Languages and Systems, 2015

Clean-Slate Development of Certified OS Kernels.
Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

A Compositional Semantics for Verified Separate Compilation and Linking.
Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

2014
Trace-Based Temporal Verification for Message-Passing Programs.
Proceedings of the 2014 Theoretical Aspects of Software Engineering Conference, 2014

A Separation Logic for Enforcing Declarative Information Flow Control Policies.
Proceedings of the Principles of Security and Trust - Third International Conference, 2014

End-to-end verification of stack-space bounds for C programs.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014

Type-Based Amortized Resource Analysis with Integers and Arrays.
Proceedings of the Functional and Logic Programming - 12th International Symposium, 2014

Compositional verification of termination-preserving refinement of concurrent programs.
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

2013
Quantitative Reasoning for Proving Lock-Freedom.
Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

Characterizing Progress Properties of Concurrent Objects via Contextual Refinements.
Proceedings of the CONCUR 2013 - Concurrency Theory - 24th International Conference, 2013

2012
A Structural Approach to Prophecy Variables.
Proceedings of the Theory and Applications of Models of Computation, 2012

Static and user-extensible proof checking.
Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Proving the correctness of concurrent robot software.
Proceedings of the IEEE International Conference on Robotics and Automation, 2012

Compositional Verification of a Baby Virtual Memory Manager.
Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

Modular Verification of Concurrent Thread Management.
Proceedings of the Programming Languages and Systems - 10th Asian Symposium, 2012

A Case for Behavior-Preserving Actions in Separation Logic.
Proceedings of the Programming Languages and Systems - 10th Asian Symposium, 2012

2011
A Simple Model for Certifying Assembly Programs with First-Class Function Pointers.
Proceedings of the 5th IEEE International Symposium on Theoretical Aspects of Software Engineering, 2011

CertiKOS: a certified kernel for secure cloud computing.
Proceedings of the APSys '11 Asia Pacific Workshop on Systems, 2011

2010
Certified software.
Commun. ACM, 2010

VeriML: typed computation of logical terms inside a language with effects.
Proceedings of the Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, 2010

Parameterized Memory Models and Concurrent Separation Logic.
Proceedings of the Programming Languages and Systems, 2010

Reasoning about Optimistic Concurrency Using a Program Logic for History.
Proceedings of the CONCUR 2010 - Concurrency Theory, 21th International Conference, 2010

2009
Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads.
J. Autom. Reasoning, 2009

Modular Development of Certified System Software.
Proceedings of the TASE 2009, 2009

Weak updates and separation logic.
Proceedings of the Programming Languages and Systems, 7th Asian Symposium, 2009

2008
Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems.
Proceedings of the Verified Software: Theories, 2008

Certifying low-level programs with hardware interrupts and preemptive threads.
Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, 2008

2007
Using XCAP to Certify Realistic Systems Code: Machine Context Management.
Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

An open framework for foundational proof-carrying code.
Proceedings of TLDI'07: 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2007

Foundational Typed Assembly Language with Certified Garbage Collection.
Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, 2007

A general framework for certifying garbage collectors and their mutators.
Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

Certified self-modifying code.
Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning.
Proceedings of the Programming Languages and Systems, 2007

2006
Certified assembly programming with embedded code pointers.
Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006

Modular verification of assembly code with stack-based control abstractions.
Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, 2006

2005
A type system for certified binaries.
ACM Trans. Program. Lang. Syst., 2005

Modular verification of concurrent assembly code with dynamic thread creation and termination.
Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, 2005

2004
Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code.
Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

Verification of safety properties for concurrent assembly code.
Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming, 2004

2003
Intensional analysis of quantified types.
ACM Trans. Program. Lang. Syst., 2003

Inlining as staged computation.
J. Funct. Program., 2003

Building Certified Libraries for PCC: Dynamic Storage Allocation.
Proceedings of the Programming Languages and Systems, 2003

Precision in Practice: A Type-Preserving Java Compiler.
Proceedings of the Compiler Construction, 12th International Conference, 2003

2002
Type-preserving compilation of Featherweight Java.
ACM Trans. Program. Lang. Syst., 2002

A type system for certified binaries.
Proceedings of the Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002

A Syntactic Approach to Foundational Proof-Carrying Code.
Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 2002

Supporting Binary Compatibility with Static Compilation.
Proceedings of the 2nd Java Virtual Machine Research and Technology Symposium, 2002

2001
Invited Talk: Towards a Principled Multi-Language Infrastructure.
Electr. Notes Theor. Comput. Sci., 2001

Principled Scavenging.
Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2001

2000
Efficient and safe-for-space closure conversion.
ACM Trans. Program. Lang. Syst., 2000

Fully reflexive intensional type analysis.
Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), 2000

1999
Transparent Modules with Fully Syntactic Signatures.
Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), 1999

Representing Java Classes in a Typed Intermediate Language.
Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), 1999

Safe and Principled Language Interoperation.
Proceedings of the Programming Languages and Systems, 1999

1998
Type-Directed Continuation Allocation.
Proceedings of the Types in Compilation, Second International Workshop, 1998

Optimal Type Lifting.
Proceedings of the Types in Compilation, Second International Workshop, 1998

Implementing Typed Intermediate Languages.
Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP '98), 1998

Typed Cross-Module Compilation.
Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP '98), 1998

1997
Flexible Representation Analysis.
Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP '97), 1997

Typed Common Intermediate Format.
Proceedings of the Conference on Domain-Specific Languages, 1997

1996
Empirical and Analytic Study of Stack Versus Heap Cost for Languages with Closures.
J. Funct. Program., 1996

1995
A Type-Based Compiler for Standard ML.
Proceedings of the ACM SIGPLAN'95 Conference on Programming Language Design and Implementation (PLDI), 1995

1994
Unrolling Lists.
Proceedings of the 1994 ACM Conference on LISP and Functional Programming, 1994

Space-Efficient Closure Representations.
Proceedings of the 1994 ACM Conference on LISP and Functional Programming, 1994

1993
Smartest Recompilation.
Proceedings of the Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1993

1992
Callee-Save Registers in Continuation-Passing Style.
Lisp and Symbolic Computation, 1992


  Loading...