Zhong Shao

Available identifiers

zbMath Open shao.zhongDBLPs/ZhongShaoWikidataQ102109405 ScholiaQ102109405MaRDI QIDQ835763

List of research outcomes

Publication	Date of Publication	Type
Automated resource analysis with Coq proof objects	2022-08-12	Paper
Refinement-Based Game Semantics for Certified Abstraction Layers	2021-01-21	Paper
Typed cross-module compilation	2019-09-26	Paper
Toward compositional verification of interruptible OS kernels and device drivers	2018-08-21	Paper
Compositional verification of termination-preserving refinement of concurrent programs	2018-04-23	Paper
Type-based amortized resource analysis with integers and arrays	2017-10-23	Paper
Certified assembly programming with embedded code pointers	2017-08-21	Paper
Flexible representation analysis	2017-08-21	Paper
Typed cross-module compilation	2017-08-21	Paper
Quantitative Reasoning for Proving Lock-Freedom	2017-07-03	Paper
Deep specifications and certified abstraction layers	2016-09-29	Paper
Representing Java classes in a typed intermediate language	2016-09-01	Paper
Transparent modules with fully syntatic signatures	2016-09-01	Paper
Automatic Static Cost Analysis for Parallel Programs	2016-04-26	Paper
Fully reflexive intensional type analysis	2015-09-11	Paper
Static and user-extensible proof checking	2015-09-11	Paper
A type system for certified binaries	2015-03-17	Paper
Verification of safety properties for concurrent assembly code	2015-03-09	Paper
VeriML	2015-03-05	Paper
Modular verification of concurrent assembly code with dynamic thread creation and termination	2015-01-06	Paper
Type-Based Amortized Resource Analysis with Integers and Arrays	2014-07-24	Paper
Characterizing Progress Properties of Concurrent Objects via Contextual Refinements	2013-08-12	Paper
Compositional Verification of a Baby Virtual Memory Manager	2013-04-19	Paper
Weak updates and separation logic	2012-11-16	Paper
A Structural Approach to Prophecy Variables	2012-07-16	Paper
Reasoning about Optimistic Concurrency Using a Program Logic for History	2010-08-31	Paper
Parameterized Memory Models and Concurrent Separation Logic	2010-05-04	Paper
Certifying low-level programs with hardware interrupts and preemptive threads	2009-08-31	Paper
Using XCAP to Certify Realistic Systems Code: Machine Context Management	2008-09-02	Paper
On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning	2007-09-04	Paper
Theorem Proving in Higher Order Logics	2005-08-18	Paper
Building certified libraries for PCC: dynamic storage allocation	2004-11-22	Paper
A syntactic approach to foundational proof-carrying code	2004-08-06	Paper
https://portal.mardi4nfdi.de/entity/Q4417787	2003-07-30	Paper
https://portal.mardi4nfdi.de/entity/Q4417905	2003-07-30	Paper
Inlining as staged computation	2003-01-01	Paper

Research outcomes over time

This page was built for person: Zhong Shao