Zhong Shao

Available identifiers

zbMath Open shao.zhongWikidataQ102109405 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
Flexible representation analysis	2017-08-21	Paper
Typed cross-module compilation	2017-08-21	Paper
Certified assembly programming with embedded code pointers	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
Static and user-extensible proof checking	2015-09-11	Paper
Fully reflexive intensional type analysis	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

Doctoral students

No records found.

Known relations from the MaRDI Knowledge Graph

Property	Value
MaRDI profile type	MaRDI person profile
instance of	human

This page was built for person: Zhong Shao