【90718026】面向携带证明软件设计的语言、逻辑和证明国家自然基金项目

面向携带证明软件设计的语言、逻辑和证明

项目批准号： 90718026

批准年份： 2007

学科分类： F0201.计算机科学的基础理论

项目负责人：陈意云

资助类别：重大研究计划

负责人职称：教授

依托单位：中国科学技术大学

资助金额： 50万元

关键词：出具证明编程语言;携带证明的代码;高可信软件;形式程序验证

起止时间： 2008-01-01到2010-12-01

中英文摘要
结题摘要
结题报告
项目成果
项目参与人

查看更多信息请先登录或注册

序号	标题	类型	作者
1	Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads (Extended Version)	期刊论文	冯新宇\|邵中\|郭宇\|董渊\|
2	Automated verification of pointer programs in pointer logic	期刊论文	Wang, Zhifang\|Chen, Yiyun\|Wang, Zhenming\|Hua, Baojian\|
3	Certifying Compiler for Clike Subset of C Language	会议论文	杨思敏\|李兆鹏\|张臻婷\|范大威\|庄重\|陈意云\|
4	一种构造代码安全性证明的方法	期刊论文	林春晓\|陈意云\|郭宇\|
5	渐进式标记-清扫垃圾收集机制验证	期刊论文	陈意云\|李隆\|林春晓\|
6	Certifying low-level programs with hardware interrupts and preemptive threads	会议论文	Dongt, Yuan\|Feng, Xinyu\|Guo, Yu\|Shao, Zhong\|
7	The Logical Approach to Low-level Stack Reasoning	会议论文	蒋信予\|郭宇\|陈意云\|
8	Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems	会议论文	郭宇\|董渊\|冯新宇\|邵中\|
9	汇编代码验证中的形式规范自动生成	期刊论文	陈意云\|葛琳\|李兆鹏\|刘诚\|华保健\|
10	Formal Reasoning about Concurrent Assembly Code with Reentrant Locks	会议论文	付明\|张昱\|李勇\|
11	一种汇编语言指针逻辑的设计与实现	期刊论文	华保健\|李兆鹏\|陈意云\|田波\|王伟\|
12	一种用于指针程序安全性证明的指针逻辑	期刊论文	陈意云\|华保健\|葛琳\|王志芳\|
13	Formal Verification of Concurrent Programs with Read-Write Locks	期刊论文	付明\|张昱\|李勇\|
14	On the verification of strong atomicity of programs using STM	会议论文	付明\|陈意云\|李勇\|张昱\|
15	验证带有线程的动态创建和退出的多线程程序	期刊论文	陈意云\|郭宇\|王海波\|
16	Certification of Thread Context Switching	期刊论文	蒋信予\|陈意云\|郭宇\|
17	一种汇编程序的形式验证框架	期刊论文	华保健\|葛琳\|李兆鹏\|陈意云\|
18	Reasoning about optimistic concurrency using a program logic for history	会议论文	张昱\|付明\|李勇\|冯新宇\|邵中\|
19	一个出具证明编译器后端的设计与实现	期刊论文	王志芳\|王伟\|陈意云\|李兆鹏\|田波\|
20	一个关于程序时间性质的验证框架	期刊论文	郭宇\|陈意云\|蒋信予\|
21	Certifying concurrent programs using transactional memory	期刊论文	Li, Yong\|Zhang, Yu\|Li, Long\|Chen, Yi-Yun\|
22	Verification of an Incremental Garbage Collector in Hoare-Style Logic	期刊论文	陈意云\|华蓓\|林春晓\|
23	一种用于指针程序验证的指针逻辑	期刊论文	王志芳\|陈意云\|李兆鹏\|华保健\|
24	处理指针相等关系不确定的指针逻辑	期刊论文	梁红瑾\|李兆鹏\|张昱\|华保健\|陈意云\|
25	An extension to Pointer Logic for verification	会议论文	Zhenming, Wang\|Wei, Wang\|Bo, Tian\|Zhifang, Wang\|Yiyun, Chen\|
26	Formal reasoning about lazy-STM programs	期刊论文	李勇\|陈意云\|张昱\|付明\|
27	A decision procedure for XPath satisfiability in the presence of DTD containing choice	会议论文	Li, Xunhao\|Zhang, Yu\|Cao, Yihua\|
28	一个用于指针程序验证的自动定理证明器的设计与实现	期刊论文	王志芳\|王振明\|陈意云\|
29	Automated theorem prover for pointer logic	期刊论文	Chen, Yi-Yun\|Wang, Zhi-Fang\|Wang, Zhen-Ming\|
30	一个经过证明的类型化汇编语言的类型检查器	期刊论文	华保健\|陈意云\|李兆鹏\|郭宇\|
31	Implementation of pointer logic for automated verification	会议论文	Wang, Zhifang\|Chen, Yiyun\|Tian, Bo\|Wang, Zhenming\|Wang, Wei\|

查看更多信息请先登录或注册

再问科研

相关项目

趋势报告

经验分享