Search results for "Zhong Shao"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
1	Zipeng Zhang, Xinyu Feng, Ming Fu, Zhong Shao, Yong Li	A Structural Approach to Prophecy Variables.	TAMC	2012	DBLP DOI BibTeX RDF
1	Antonis Stampoulis, Zhong Shao	Static and user-extensible proof checking.	POPL	2012	DBLP DOI BibTeX RDF
1	Gang Tan, Zhong Shao, Xinyu Feng, Hongxu Cai	Weak Updates and Separation Logic.	New Generation Comput.	2011	DBLP DOI BibTeX RDF
1	Jean-Pierre Jouannaud, Zhong Shao (eds.)	Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings	CPP	2011	DBLP DOI BibTeX RDF
1	Wei Wang, Zhong Shao, Xinyu Jiang, Yu Guo	A Simple Model for Certifying Assembly Programs with First-Class Function Pointers.	TASE	2011	DBLP DOI BibTeX RDF
1	Liang Gu, Alexander Vaynberg, Bryan Ford, Zhong Shao, David Costanzo	CertiKOS: a certified kernel for secure cloud computing.	APSys	2011	DBLP DOI BibTeX RDF
1	Zhong Shao	Certified software.	Commun. ACM	2010	DBLP DOI BibTeX RDF
1	Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, Yu Zhang	Reasoning about Optimistic Concurrency Using a Program Logic for History.	CONCUR	2010	DBLP DOI BibTeX RDF
1	Antonis Stampoulis, Zhong Shao	VeriML: typed computation of logical terms inside a language with effects.	ICFP	2010	DBLP DOI BibTeX RDF
1	Rodrigo Ferreira, Xinyu Feng, Zhong Shao	Parameterized Memory Models and Concurrent Separation Logic.	ESOP	2010	DBLP DOI BibTeX RDF
1	Xinyu Feng, Zhong Shao, Yu Guo, Yuan Dong	Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Operating system verification, Hardware interrupts, Preemptive threads, Thread libraries, Modularity, Separation logic, Synchronization primitives
1	Zhong Shao, Benjamin C. Pierce (eds.)	Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009	POPL	2009	DBLP BibTeX RDF
1	Gang Tan, Zhong Shao, Xinyu Feng, Hongxu Cai	Weak updates and separation logic.	APLAS	2009	DBLP DOI BibTeX RDF
1	Zhong Shao	Modular Development of Certified System Software.	TASE	2009	DBLP DOI BibTeX RDF
1	Xinyu Feng, Zhong Shao, Yuan Dong, Yu Guo	Certifying low-level programs with hardware interrupts and preemptive threads.	PLDI	2008	DBLP DOI BibTeX RDF	certified system software, hardware interrupts, preemptive threads, concurrency, separation logic
1	Xinyu Feng, Zhong Shao, Yu Guo, Yuan Dong	Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems.	VSTTE	2008	DBLP DOI BibTeX RDF
1	Hongxu Cai, Zhong Shao, Alexander Vaynberg	Certified self-modifying code.	PLDI	2007	DBLP DOI BibTeX RDF	assembly code verification, runtime code manipulation, self-modifying code, hoare logic, modular verification
1	Andrew McCreight, Zhong Shao, Chunxiao Lin, Long Li	A general framework for certifying garbage collectors and their mutators.	PLDI	2007	DBLP DOI BibTeX RDF	assembly code verification, garbage collection, abstract data type, separation logic, proof-carrying code
1	Xinyu Feng, Zhaozhong Ni, Zhong Shao, Yu Guo	An open framework for foundational proof-carrying code.	TLDI	2007	DBLP DOI BibTeX RDF	foundational proof-carrying code, open framework, interoperability, modularity, program verification
1	Zhaozhong Ni, Dachuan Yu, Zhong Shao	Using XCAP to Certify Realistic Systems Code: Machine Context Management.	TPHOLs	2007	DBLP DOI BibTeX RDF
1	Zhong Shao (eds.)	Programming Languages and Systems, 5th Asian Symposium, APLAS 2007, Singapore, November 29-December 1, 2007, Proceedings	APLAS	2007	DBLP BibTeX RDF
1	Chunxiao Lin, Andrew McCreight, Zhong Shao, Yiyun Chen, Yu Guo	Foundational Typed Assembly Language with Certified Garbage Collection.	TASE	2007	DBLP DOI BibTeX RDF
1	Xinyu Feng, Rodrigo Ferreira, Zhong Shao	On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning.	ESOP	2007	DBLP DOI BibTeX RDF
1	Xinyu Feng, Zhong Shao, Alexander Vaynberg, Sen Xiang, Zhaozhong Ni	Modular verification of assembly code with stack-based control abstractions.	PLDI	2006	DBLP DOI BibTeX RDF	assembly code verification, control abstractions, stack-based, modularity, proof-carrying code
1	Zhaozhong Ni, Zhong Shao	Certified assembly programming with embedded code pointers.	POPL	2006	DBLP DOI BibTeX RDF	embedded code pointers, hoare logic, proof-carrying code, higher-order functions
1	Zhong Shao, Valery Trifonov, Bratin Saha, Nikolaos Papaspyrou	A type system for certified binaries.	ACM Trans. Program. Lang. Syst.	2005	DBLP DOI BibTeX RDF	proof-preserving compilation, typed intermediate languages, Certified code
1	Xinyu Feng, Zhong Shao	Modular verification of concurrent assembly code with dynamic thread creation and termination.	ICFP	2005	DBLP DOI BibTeX RDF	concurrency verification, dynamic thread creation, proof-carrying code, rely-guarantee
1	Dachuan Yu, Nadeem Abdul Hamid, Zhong Shao	Building certified libraries for PCC: dynamic storage allocation.	Sci. Comput. Program.	2004	DBLP DOI BibTeX RDF
1	Dachuan Yu, Zhong Shao	Verification of safety properties for concurrent assembly code.	ICFP	2004	DBLP DOI BibTeX RDF	local guarantee, concurrency, assembly
1	Nadeem Abdul Hamid, Zhong Shao	Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Bratin Saha, Valery Trifonov, Zhong Shao	Intensional analysis of quantified types.	ACM Trans. Program. Lang. Syst.	2003	DBLP DOI BibTeX RDF	intensional type analysis, runtime type dispatch, typed intermediate languages, Certified code
1	Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni	A Syntactic Approach to Foundational Proof-Carrying Code.	J. Autom. Reasoning	2003	DBLP DOI BibTeX RDF	foundational proof-carrying code, syntactic soundness proof, typed assembly language
1	Stefan Monnier, Zhong Shao	Inlining as staged computation.	J. Funct. Program.	2003	DBLP DOI BibTeX RDF
1	Zhong Shao, Peter Lee (eds.)	Proceedings of TLDI'03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, New Orleans, Louisiana, USA, January 18, 2003	TLDI	2003	DBLP BibTeX RDF
1	Christopher League, Zhong Shao, Valery Trifonov	Precision in Practice: A Type-Preserving Java Compiler.	CC	2003	DBLP DOI BibTeX RDF
1	Dachuan Yu, Nadeem Abdul Hamid, Zhong Shao	Building Certified Libraries for PCC: Dynamic Storage Allocation.	ESOP	2003	DBLP DOI BibTeX RDF
1	Christopher League, Zhong Shao, Valery Trifonov	Type-preserving compilation of Featherweight Java.	ACM Trans. Program. Lang. Syst.	2002	DBLP DOI BibTeX RDF	object encodings, Java, type systems, typed intermediate languages
1	Dachuan Yu, Zhong Shao, Valery Trifonov	Supporting Binary Compatibility with Static Compilation.	Java Virtual Machine Research and Technology Symposium	2002	DBLP BibTeX RDF
1	Zhong Shao, Bratin Saha, Valery Trifonov, Nikolaos Papaspyrou	A type system for certified binaries.	POPL	2002	DBLP DOI BibTeX RDF
1	Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni	A Syntactic Approach to Foundational Proof-Carrying Code.	LICS	2002	DBLP DOI BibTeX RDF
1	Zhong Shao	Invited Talk: Towards a Principled Multi-Language Infrastructure.	Electr. Notes Theor. Comput. Sci.	2001	DBLP DOI BibTeX RDF
1	Stefan Monnier, Bratin Saha, Zhong Shao	Principled Scavenging.	PLDI	2001	DBLP DOI BibTeX RDF
1	Zhong Shao, Andrew W. Appel	Efficient and safe-for-space closure conversion.	ACM Trans. Program. Lang. Syst.	2000	DBLP DOI BibTeX RDF	callee-save registers, closure representation, heap-based compilation, space safety, compiler optimization, flow analysis, closure conversion
1	Valery Trifonov, Bratin Saha, Zhong Shao	Fully reflexive intensional type analysis.	ICFP	2000	DBLP DOI BibTeX RDF	runtime type dispatch, typed intermediate language, certified code
1	Christopher League, Zhong Shao, Valery Trifonov	Representing Java Classes in a Typed Intermediate Language.	ICFP	1999	DBLP DOI BibTeX RDF
1	Zhong Shao	Transparent Modules with Fully Syntactic Signatures.	ICFP	1999	DBLP DOI BibTeX RDF
1	Valery Trifonov, Zhong Shao	Safe and Principled Language Interoperation.	ESOP	1999	DBLP DOI BibTeX RDF
1	Zhong Shao, Christopher League, Stefan Monnier	Implementing Typed Intermediate Languages.	ICFP	1998	DBLP DOI BibTeX RDF
1	Zhong Shao	Typed Cross-Module Compilation.	ICFP	1998	DBLP DOI BibTeX RDF
1	Zhong Shao, Valery Trifonov	Type-Directed Continuation Allocation.	Types in Compilation	1998	DBLP DOI BibTeX RDF
1	Bratin Saha, Zhong Shao	Optimal Type Lifting.	Types in Compilation	1998	DBLP DOI BibTeX RDF
1	Zhong Shao	Flexible Representation Analysis.	ICFP	1997	DBLP DOI BibTeX RDF
1	Zhong Shao	Typed Common Intermediate Format.	DSL	1997	DBLP BibTeX RDF
1	Andrew W. Appel, Zhong Shao	Empirical and Analytic Study of Stack Versus Heap Cost for Languages with Closures.	J. Funct. Program.	1996	DBLP DOI BibTeX RDF
1	Zhong Shao, Andrew W. Appel	A Type-Based Compiler for Standard ML.	PLDI	1995	DBLP DOI BibTeX RDF	Standard ML
1	Zhong Shao, John H. Reppy, Andrew W. Appel	Unrolling Lists.	LISP and Functional Programming	1994	DBLP DOI BibTeX RDF
1	Zhong Shao, Andrew W. Appel	Space-Efficient Closure Representations.	LISP and Functional Programming	1994	DBLP DOI BibTeX RDF	Standard ML
1	Zhong Shao, Andrew W. Appel	Smartest Recompilation.	POPL	1993	DBLP DOI BibTeX RDF	ML
1	Andrew W. Appel, Zhong Shao	Callee-Save Registers in Continuation-Passing Style.	Lisp and Symbolic Computation	1992	DBLP BibTeX RDF

Publications of "Zhong Shao" ( http://dblp.L3S.de/Authors/Zhong_Shao )