郭宇(中國科學技術大學計算機學院特任副教授)

郭宇，男，1979年4月生，博士，2001年畢業於南京航空航天大學，獲學士學位；2007年畢業於中國科學技術大學，獲博士學位。現任中國科學技術大學計算機學院特任副教授。

基本介紹

• 中文名：郭宇
• 出生日期：1979年4月生
• 學位/學歷：博士
• 性別：男

個人簡介

郭宇，男，1979年4月生，博士，2001年畢業於南京航空航天大學，獲學士學位；2007年畢業於中國科學技術大學，獲博士學位。現任中國科學技術大學計算機學院特任副教授。主要從事程式驗證、作業系統、程式設計語言理論方面的研究。作為骨幹先後參與了多項國家自然科學基金研究項目。

主要研究方向

程式驗證、作業系統、程式設計語言理論

主要論著

[01]	Wei Wang, Zhong Shao, Xinyu Jiang and Yu Guo. A Simple Model for Certifying Assembly Programs with First-Class Function Pointers. In Proceedings of International Symposium on Theoretical Aspects of Software Engineering(TASE'11). 2011. To appear.
[02]	Yu Guo, Xinyu Jiang, Yi-Yun Chen. Certification of Thread Context Switching. Journal of Computer Science and Technology. 25(4), 827-840.
[03]	Xinyu Feng, Zhong Shao, Yu Guo and Yuan Dong. Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. Journal of Automated Reasoning (Special Issue on Operating System Verification) 42 (2-4): 301-347, April 2009. Springer.
[04]	Xinyu. Jiang, Yu Guo and Yiyun Chen. The Logical Approach to Low-level Stack Reasoning. In Proceedings of International Symposium on Theoretical Aspects of Software Engineering(TASE'09). pages 209-216, 2009. IEEE Computer Society.
[05]	郭宇, 陳意雲, 林春曉. 一種構造代碼安全性證明的方法. 軟體學報, 19(10), pp. 2720-2727, 2008.10.
[06]	郭宇, 陳意雲, 華保健, 李兆鵬. 一個經過證明的類型化彙編語言的類型檢查器. 小型微型計算機系統, 29(7), pp. 1230-1236, 2008.7.
[07]	Xinyu Feng, Zhong Shao, Yuan Dong and Yu Guo. Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. In Proceedings of 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'08), Tucson, Arizona, pages 170-182, June 2008. ACM Press.
[08]	Xinyu Feng, Zhong Shao, Yu Guo and Yuan Dong. Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. In Proceedings of 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. Springer-Verlag.
[09]	Xinyu Feng, Zhaozhong Ni, Zhong Shao and Yu Guo. An Open Framework for Foundational Proof-Carrying Code. In Proceedings of the 3rd ACM Workshop on Types in Language Design and Implementation (TLDI '07),pages 67-78, Nice, France, Jan 2007. ACM Press.
[10]	Yu Guo, Xinyu Jiang, Yiyun Chen and Chunxiao Lin. A Certified Thread Library for Multithreaded User Programs. In Proceedings of International Symposium on Theoretical Aspects of Software Engineering(TASE '07), pages 127-136, Jun 2007. IEEE Computer Society.
[11]	Chunxiao Lin, Andrew McCreight, Zhong Shao, Yiyun Chen and Yu Guo. Foundational Typed Assembly Language with Certified Garbage Collection. In Proceedings of International Symposium on Theoretical Aspects of Software Engineering (TASE '07), pages 326-335, Jun 2007. IEEE Computer Society.