检索结果-内蒙古大学图书馆

Formal verification of a programming logic for a distributed programming language

THEORETICAL COMPUTER SCIENCE 1999年第1-2期216卷 213-235页

作者： Zhang, C Olsson, RA Levitt, KN Calif State Univ Sacramento Dept Comp Sci Sacramento CA 95819 USA Univ Calif Davis Dept Comp Sci Davis CA 95616 USA

This paper presents a method for mechanically proving the soundness of a programming logic for a distributed programming language, in support of the development of verified program verification tools. We focus on: (1) how to formalize the operational semantics of a distributed programming language;(2) how to formalize the concept of program correctness for distributed programs;(3) how to mechanically prove the soundness of a programming logic with respect to the formal semantics of the language;(4) how to use the mechanized and sound logic to develop verification tools with soundness guaranteed;and (5) how to accomplish all above in the same formalism. Our programming logic permits the verification of single processes executing in isolation and, also, the verification of the composition of concurrently executing processes. Our method demonstrates that structuring the specification of operational semantics can ease the creation of a sound and mechanized programming logic for distributed programming languages. We believe that our method can be scaled up to larger distributed programming languages and their programming logics. The Cambridge HOL theorem proving system is used in our research. (C) 1999-Elsevier Science B.V. All rights reserved.

关键词： semantic formalization mechanization of programming logics distributed programming languages machine-checked verification

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：