期刊导航
期刊开放获取
河南省图书馆
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
2
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式:
文摘
详细
列表
相关度排序
被引量排序
时效性排序
在可信编译器设计中实践CompCert编译器的语法分析器形式化验证过程
被引量:
2
1
作者
李凌
李璜华
王生原
《计算机科学》
CSCD
北大核心
2020年第6期8-15,共8页
Jourdan等在其2012年发表的论文“Validating LR(1)Parsers”中提出了一种形式化验证语法分析器的方法,并将其成功地应用于CompCert编译器(2.3以上版本)的语法分析器验证中。借助这种方法,文中完成了L2C项目中的Lustre*语言语法分析器...
Jourdan等在其2012年发表的论文“Validating LR(1)Parsers”中提出了一种形式化验证语法分析器的方法,并将其成功地应用于CompCert编译器(2.3以上版本)的语法分析器验证中。借助这种方法,文中完成了L2C项目中的Lustre*语言语法分析器的形式化验证,实现了开源L2C编译器前端语法分析器的两个选项之一。首先对这一语法分析器的实现进行了论述,其中包括有参考价值的技术细节;随后分析了该语法分析器的运行性能及正确性;最后对如何将这一方法推广至更一般的应用场景进行了总结。
展开更多
关键词
语法分析
LR(1)分析器
形式化验证
Lustre*语言
CompCert
COQ
下载PDF
职称材料
一种包解析器硬件配置描述语言及其编译结构
被引量:
1
2
作者
李璜华
李凌
+2 位作者
赵宇
王生原
李翔宇
《软件学报》
EI
CSCD
北大核心
2020年第8期2285-2308,共24页
设计了一种用于实现可重构网络数据包解析器的专用硬件配置描述语言P3.由于要有利于高安全等级网络的实现,侧重于从高可信性角度进行语言设计,包括形式化定义该语言的类型系统和操作语义,以及设计其可信编译结构.基于对可重构硬件基本...
设计了一种用于实现可重构网络数据包解析器的专用硬件配置描述语言P3.由于要有利于高安全等级网络的实现,侧重于从高可信性角度进行语言设计,包括形式化定义该语言的类型系统和操作语义,以及设计其可信编译结构.基于对可重构硬件基本需求的充分理解,从软硬件协同角度出发,最终明确了P3语言的核心特性及其编译器P3C的可信编译结构.由于可重构数据包解析器是软件定义网络(SDN)、可编程数据平面的重要一环,因此,实现P3C的可信编译结构将对SDN的安全性具有重大意义.期待P3C项目的开展能够促进网络与形式化领域相关工作的进一步研究.
展开更多
关键词
领域专用语言
可重构数据包解析器
形式语义
可信编译
软件定义网络
下载PDF
职称材料
题名
在可信编译器设计中实践CompCert编译器的语法分析器形式化验证过程
被引量:
2
1
作者
李凌
李璜华
王生原
机构
清华大学计算机科学与技术系
出处
《计算机科学》
CSCD
北大核心
2020年第6期8-15,共8页
基金
核高基重大专项(2017ZX01030-301-003)。
文摘
Jourdan等在其2012年发表的论文“Validating LR(1)Parsers”中提出了一种形式化验证语法分析器的方法,并将其成功地应用于CompCert编译器(2.3以上版本)的语法分析器验证中。借助这种方法,文中完成了L2C项目中的Lustre*语言语法分析器的形式化验证,实现了开源L2C编译器前端语法分析器的两个选项之一。首先对这一语法分析器的实现进行了论述,其中包括有参考价值的技术细节;随后分析了该语法分析器的运行性能及正确性;最后对如何将这一方法推广至更一般的应用场景进行了总结。
关键词
语法分析
LR(1)分析器
形式化验证
Lustre*语言
CompCert
COQ
Keywords
Syntax parsing
LR(1)parser
Formal verification
Lustre*language
CompCert
Coq
分类号
TP314 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
一种包解析器硬件配置描述语言及其编译结构
被引量:
1
2
作者
李璜华
李凌
赵宇
王生原
李翔宇
机构
清华大学计算机科学与技术系
北京信息科技大学理学院
清华大学微电子学研究所
出处
《软件学报》
EI
CSCD
北大核心
2020年第8期2285-2308,共24页
基金
核高基国家科技重大专项(2017ZX01030-301-003)。
文摘
设计了一种用于实现可重构网络数据包解析器的专用硬件配置描述语言P3.由于要有利于高安全等级网络的实现,侧重于从高可信性角度进行语言设计,包括形式化定义该语言的类型系统和操作语义,以及设计其可信编译结构.基于对可重构硬件基本需求的充分理解,从软硬件协同角度出发,最终明确了P3语言的核心特性及其编译器P3C的可信编译结构.由于可重构数据包解析器是软件定义网络(SDN)、可编程数据平面的重要一环,因此,实现P3C的可信编译结构将对SDN的安全性具有重大意义.期待P3C项目的开展能够促进网络与形式化领域相关工作的进一步研究.
关键词
领域专用语言
可重构数据包解析器
形式语义
可信编译
软件定义网络
Keywords
domain-specific language
reconfigurable packet parser
formal semantics
trustworthy compiler
software-defined networking
分类号
TP314 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
在可信编译器设计中实践CompCert编译器的语法分析器形式化验证过程
李凌
李璜华
王生原
《计算机科学》
CSCD
北大核心
2020
2
下载PDF
职称材料
2
一种包解析器硬件配置描述语言及其编译结构
李璜华
李凌
赵宇
王生原
李翔宇
《软件学报》
EI
CSCD
北大核心
2020
1
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部