Publications

Published papers, technical reports, and talks online.


Listed in reverse chronological order. This BibTeX file contains entries for some publications listed on this page.

Automated Resource Analysis with Coq Proof Objects. Quentin Carbonneaux, Jan Hoffmann, Thomas Reps, and Zhong Shao. In Proc. 29th International Conference on Computer Aided Verification (CAV 2017), Heidelberg, Germany, Part II, pages 64-85, July 2017.

CertiKOS: An Extenisble Architecture for Building Certified Concurrent OS Kernels. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. In Proc. 2016 USENIX Symposium on Operating Systems Design and Implementation (OSDI'16), Savannah, GA, pages 653-669, November 2016.

Toward Compositional Verification of Interruptible OS Kernels and Device Drivers. Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, and Ronghui Gu. In Proc. 2016 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'16), Santa Barbara, CA, pages 431-447, June 2016.

End-to-End Verification of Information-Flow Security for C and Assembly Programs. David Costanzo, Zhong Shao, and Ronghui Gu. In Proc. 2016 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'16), Santa Barbara, CA, pages 648-664, June 2016.

Compositional Certified Resource Bounds. Quentin Carbonneaux, Jan Hoffmann, and Zhong Shao. In Proc. 2015 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15), Portland, OR, pages 467-478, June 2015.

Automatic Static Cost Analysis for Parallel Programs. Jan Hoffmann and Zhong Shao. In Proc. 24th European Symposium on Programming (ESOP'15), London, UK, April 2015. Lecture Notes in Computer Science, Vol. 9032, pages 132-157.

Deep Specifications and Certified Abstraction Layers. Ronghui Gu, Jérémie_Koenig, Tahina_Ramananandro, Zhong_Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. In Proc. 42nd ACM Symposium on Principles of Programming Languages (POPL'15), Mumbia, India, pages 595-608, January 2015.

A Compositional Semantics for Verified Separate Compilation and Linking. Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jérémie Koenig, and Yuchen Fu. In Proc. 4th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP'15), Mumbia, India, pages 3-14, January 2015.

Compositional Verification of Termination-Preserving Refinement of Concurrent Programs. Hongjin Liang, Xinyu Feng, and Zhong Shao. In Proc. 23rd EACSL Annual Conference on Computer Science Logic and 29th Annual IEEE Symposium on Logic in Computer Science (CSL-LICS'14), Vienna, Austria, Paper No. 65, July 2014. ©2014 IEEE Computer Society.

End-to-End Verification of Stack-Space Bounds for C Programs. Quentin Carbonneaux, Jan Hoffmann, Tahina Ramananandro, and Zhong Shao. In Proc. 2014 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'14), Edinburgh, UK pages 270-281, June 2014. ©2014 ACM.

Type-Based Amortized Resource Analysis with Integers and Arrays, Jan Hoffmann and Zhong Shao In Proc. 12th International Symosium on Functional and Logic Programming (FLOPS'14), Kanazawa, Japan, June 2014. Lecture Notes in Computer Science, Vol. 8475, pages 152-168. © 2014 Springer-Verlag.

A Separation Logic for Enforcing Declarative Information Flow Control Policies, David Costanzo and Zhong Shao In Proc. 3rd Conference on Principles of Security and Trust (POST'14), Grenoble, France, April 2014. Lecture Notes in Computer Science, Vol. 8414, pages 179-198. © 2014 Springer-Verlag.

Characterizing Progress Properties of Concurrent Objects via Contextual Refinements, Hongjin Liang, Jan Hoffmann, Xinyu Feng, and Zhong Shao. In Proc. 24th International Conference on Concurrency Theory (CONCUR'13), Buenos Aires, Argentina, August 2013. Lecture Notes in Computer Science Vol. 8052, pages 227-241. © 2013 Springer-Verlag.

Quantitative Reasoning for Proving Lock-Freedom. Jan Hoffmann, Michael Marmar, and Zhong Shao. In Proc. 28th Annual IEEE Symposium on Logic in Computer Science (LICS'13), New Orleans, USA, pages 124-133, June 2013. ©2013 IEEE Computer Society.

Compositional Verification of a Baby Virtual Memory Manager, Alexander Vaynberg and Zhong Shao. In Proc. 2nd International Conference on Certified Programs and Proofs (CPP'12), Kyoto, Japan, December 2012. Lecture Notes in Computer Science Vol. (TBA), pages (TBA). © 2012 Springer-Verlag.

A Case for Behavior-Preserving Actions in Separation Logic, David Costanzo and Zhong Shao. In Proc. 10th Asian Symposium on Programming Languages and Systems (APLAS'12), Kyoto, Japan, December 2012. Lecture Notes in Computer Science Vol. 7705, pages (TBA). © 2012 Springer-Verlag.

Modular Verification of Concurrent Thread Management, Yu Guo, Xinyu Feng, Zhong Shao, and Peizhi Shi. In Proc. 10th Asian Symposium on Programming Languages and Systems (APLAS'12), Kyoto, Japan, December 2012. Lecture Notes in Computer Science Vol. 7705, pages (TBA). © 2012 Springer-Verlag.

Static and User-Extensible Proof Checking. Antonis Stampoulis and Zhong Shao. In Proc. 39th ACM Symposium on Principles of Programming Languages (POPL'12), Philadelphia, Pennsylvania, pages 273-284, January 2012. © 2012 ACM.

A Simple Model for Certifying Assembly Programs with First-Class Function Pointers. Wei Wang, Zhong Shao, Xinyu Jiang, and Yu Guo. In Proc. 4th IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE'11), Xian, China, pages 125-132, August 2011. © 2011 IEEE Computer Society.

CertiKOS: A Certified Kernel for Secure Cloud Computing. Liang Gu, Alexander Vaynberg, Bryan Ford, Zhong Shao, and David Costanzo. In Proc. 2nd ACM SIGOPS Asia-Pacific Workshop on Systems (APSys'11), Shanghai, China, July 2011. © 2011 ACM.

Certifying the Concurrent State Table Implementation in a Surgical Robotic System (Extended Version). Yanni Kouskoulas, Ming Fu, Zhong Shao, and Peter Kazanzides. A shorter summary of this paper appeared in Proc. 3rd Joint Workshop on High Confidence Medical Devices, Software, and Systems & Medical Device Plug-and-Play Interoperability, Chicago, USA. June 2011.

Weak Updates and Separation Logic. Gang Tan, Zhong Shao, Xinyu Feng, and Hongxu Cai. In New Generation Computing: Computing Paradigms and Computational Intelligence , Volume 29, No. 1, 2011, pages 1-29. © Ohmsha, Ltd. and Springer 2011. An earlier version appeared in Proc. 7th Asian Symposium on Programming Languages and Systems (APLAS'09), Seoul, Korea, December 2009. Lecture Notes in Computer Science Vol. 5904, pages 178-193.

Certified Software, Zhong Shao. In Communications of the ACM, 53(12), pages 56-66, December 2010. © 2010 ACM.

VeriML: Typed Computation of Logical Terms inside a Language with Effects, Antonis Stampoulis and Zhong Shao. In Proc. 2010 ACM SIGPLAN International Conference on Functional Programming (ICFP'10), Baltimore, Maryland, pages 333-344, September 2010. © 2010 ACM.

Reasoning about Optimistic Concurrency Using a Program Logic for History, Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, and Yu Zhang. In Proc. 21st International Conference on Concurrency Theory (CONCUR'10), Paris, France, August 2010. Lecture Notes in Computer Science Vol. 6269, pages 388-402. © 2010 Springer-Verlag.

Advanced Development of Certified OS Kernels. Zhong Shao and Bryan Ford. Technical Report YALEU/DCS/TR-1436, Department of Computer Science, Yale University, July 2010.

Memory Consistency and Program Verification. Rodrigo Ferreira, Ph.D. dissertation, Department of Computer Science, Yale University, April 2010.

Parametrized Memory Models and Concurrent Separation Logic, Rodrigo Ferreira, Xinyu Feng, and Zhong Shao. In Proc. 19th European Symposium on Programming (ESOP'10), Paphos, Cyprus, March 2010. Lecture Notes in Computer Science Vol. 6012, pages 267-286. © 2010 Springer-Verlag.

Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads (Extended Version). Xinyu Feng, Zhong Shao, Yu Guo, and Yuan Dong. Journal of Automated Reasoning (Special Issue on Operating System Verification) 42 (2-4): 301-347, April 2009. © Springer Science + Business Media B.V.2009.

Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. Xinyu Feng, Zhong Shao, Yu Guo and Yuan Dong. In Proc. Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'08), Toronto, Canada, October 2008. Lecture Notes in Computer Science Vol. 5295, pages 54-69. © 2008 Springer-Verlag.

The Mechanized Verification of Garbage Collector Implementations. Andrew McCreight, Ph.D. dissertation, Department of Computer Science, Yale University, December 2008.

Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. Xinyu Feng, Zhong Shao, Yuan Dong and Yu Guo. In Proc. 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'08), Tucson, Arizona, pages 170-182, June 2008. © 2008 ACM.

An Open Framework for Certified System Software. Xinyu Feng, Ph.D. dissertation, Department of Computer Science, Yale University, December 2007.

Using XCAP to Certify Realistic System Code: Machine Context Management. Zhaozhong Ni, Dachuan Yu, and Zhong Shao. In Proc. 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'07) , Kaiserslautern, Germany, September 2007. Lecture Notes in Computer Science Vol. 4732, pages 189-206. © 2007 Springer-Verlag.

Certified Self-Modifying Code. Hongxu Cai, Zhong Shao, and Alexander Vaynberg. In Proc. 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'07), San Diego, CA, pages 66-77, June 2007. © 2007 ACM.

A General Framework for Certifying Garbage Collectors and Their Mutators. Andrew McCreight, Zhong Shao, Chunxiao Lin, and Long Li. In Proc. 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'07), San Diego, CA, pages 468-479, June 2007. © 2007 ACM.

Foundational Typed Assembly Language with Certified Garbage Collection. Chunxiao Lin, Andrew McCreight, Zhong Shao, Yiyun Chen, and Yu Guo. In Proc. 1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE'07), Shanghai, China, pages 326-335, June 2007. © 2007 IEEE Computer Society.

On the Relationship between Concurrent Separation Logic and Assume-Guarantee Reasoning Xinyu Feng, Rodrigo Ferreira, and Zhong Shao. In Proc. 16th European Symposium on Programming (ESOP'07), Braga, Portugal, March 2007. Lecture Notes in Computer Science Vol. 4421, pages 173-188. © 2007 Springer-Verlag.

An Open Framework for Foundational Proof-Carrying Code. Xinyu Feng, Zhaozhong Ni, Zhong Shao, and Yu Guo. In Proc. 2007 ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI'07) , Nice, France, pages 67-78, January 2007. © 2007 ACM.

Modular Machine Code Verification. Zhaozhong Ni, Ph.D. dissertation, Department of Computer Science, Yale University, November 2006.

Modular Verification of Assembly Code with Stack-Based Control Abstractions. Xinyu Feng, Zhong Shao, Alexander Vaynberg, Sen Xiang, and Zhaozhong Ni. In Proc. 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'06), Ottawa, Canada, pages 401-414, June 2006. © 2006 ACM.

Certified Assembly Programming with Embedded Code Pointers. Zhaozhong Ni and Zhong Shao. In Proc. 33rd ACM Symposium on Principles of Programming Languages (POPL'06), Charleston, South Carolina, pages 320-333, January 2006. © 2006 ACM.

Modular Verification of Concurrent Assembly Code with Dynamic Thread Creation and Termination. Xinyu Feng and Zhong Shao. In Proc. 2005 ACM SIGPLAN International Conference on Functional Programming (ICFP'05), Tallinn, Estonia, pages 254-267, September 2005. © 2005 ACM.

A Type System for Certified Binaries. Zhong Shao, Valery Trifonov, Bratin Saha, and Nikolaos Papaspyrou. In ACM Transactions on Programming Languages and Systems (TOPLAS), 27(1), pages 1-45, January 2005. © 2005 ACM.

Verification of Safety Properties for Concurrent Assembly Code. Dachuan Yu and Zhong Shao. In Proc. 2004 ACM SIGPLAN International Conference on Functional Programming (ICFP'04), Snowbird, Utah, pages 175-188, September 2004. © 2004 ACM.

Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code. Nadeem A. Hamid and Zhong Shao. In Proc. 17th International Conference on the Applications of Higher Order Logic Theorem Proving (TPHOLs'04), Park City, Utah, September 2004. Lecture Notes in Computer Science Vol. 3223, pages 118-135. © 2004 Springer-Verlag.

Building Certified Libraries for PCC: Dynamic Storage Allocation (Extended Version). Dachuan Yu, Nadeem A. Hamid, and Zhong Shao. In Science of Computer Programming (Special Issue ESOP 2003), 50 (1-3): 101-127, March 2004. © 2004 Elsevier.

A Syntactic Approach to Foundational Proof-Carrying Code (Extended Version). Nadeem A. Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, and Zhaozhong Ni. Journal of Automated Reasoning (Special Issue on Proof-Carrying Code) 31 (3-4): 191-229, 2003.

Building Certified Libraries for PCC: Dynamic Storage Allocation. Dachuan Yu, Nadeem A. Hamid, and Zhong Shao. In Proc. 2003 European Symposium on Programming (ESOP'03), Warsaw, Poland, April 2003. Lecture Notes in Computer Science Vol. 2618. © Springer-Verlag. (Also available as Technical Report YALEU/DCS/TR-1247, Department of Computer Science, Yale University, January 2003).

Precision in Practice: A Type-Preserving Java Compiler. Christopher League, Zhong Shao, and Valery Trifonov. In Proc. 12th International Conference on Compiler Construction (CC'03), Warsaw, Poland, April 2003. Lecture Notes in Computer Science Vol. 2622. © Springer-Verlag.

Typed Regions. Stefan Monnier and Zhong Shao. Technical Report YALEU/DCS/TR-1242, Department of Computer Science, Yale University, October 2002.

Intensional Analysis of Higher-Kinded Recursive Types. Gregory D. Collins and Zhong Shao. Technical Report YALEU/DCS/TR-1240, Department of Computer Science, Yale University, October 2002.

A Type-Preserving Compiler Infrastructure. Christopher League, Ph.D. dissertation.

A Type System For Certified Runtime Type Analysis. Bratin Saha, Ph.D. dissertation.

Intensional Analysis of Quantified Types. Bratin Saha, Valery Trifonov, and Zhong Shao. In ACM Transactions on Programming Languages and Systems (TOPLAS), 25(2), pages 159-209, March 2003. © 2003 ACM.

Supporting Binary Compatibility with Static Compilation. Dachuan Yu, Zhong Shao, and Valery Trifonov. In USENIX 2nd Java[TM] Virtual Machine Research and Technology Symposium (JVM'02), San Francisco, California, pages 165-180, August 2002. Winner of the Best Student Paper Award. © 2002 USENIX.

A Syntactic Approach to Foundational Proof-Carrying Code. Nadeem A. Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, and Zhaozhong Ni. In Proc. 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), Copenhagen, Denmark, pages 89-100, July 2002. © 2007 IEEE Computer Society.

Type-Preserving Compilation of Featherweight IL. Dachuan Yu, Valery Trifonov, Zhong Shao. In Proc. 2002 Workshop on Formal Techniques for Java-like Programs (FTfJP'02), Malaga, Spain, June 2002. (Also available as Technical Report YALEU/DCS/TR-1228, Department of Computer Science, Yale University, April 2002).

Type-Preserving Compilation of Featherweight Java. Christopher League, Zhong Shao, and Valery Trifonov. In ACM Transactions on Programming Languages and Systems (TOPLAS), 24(2), pages 112-152, March 2002. © 2002 ACM.

A Type System for Certified Binaries. Zhong Shao, Bratin Saha, Valery Trifonov, and Nikolaos Papaspyrou. In Proc. 29th ACM Symposium on Principles of Programming Languages (POPL'02), Portland, OR, pages 217-232, January 2002, © 2002 ACM.

A Type System for Certified Binaries (Extended Version). Zhong Shao, Bratin Saha, Valery Trifonov, and Nikolaos Papaspyrou. Technical Report YALEU/DCS/TR-1211, Department of Computer Science, Yale University, March 2001 (revised September 2001).

Inlining as Staged Computation. Stefan Monnier and Zhong Shao. In Journal of Functional Programming, 13(3), pages 647-676, May 2003. © 2003 Cambridge University Press.

Functional Java Bytecode. Christopher League, Valery Trifonov, and Zhong Shao. In Proc. 2001 Workshop on Intermediate Representation Engineering for the Java Virtual Machine at the 5th World Multi-conference on Systemics, Cybernetics, and Informatics, Orlando, FL, July 2001.

Principled Scavenging. Stefan Monnier, Bratin Saha, and Zhong Shao. In Proc. 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'01), Snowbird, UT, pages 81-91, June 2001. © 2001 ACM.