• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>IEEE International Symposium on Theoretical Aspects of Software Engineering >A Certifying Compiler for Clike Subset of C Language
【24h】

A Certifying Compiler for Clike Subset of C Language

机译：C语言CLIKE子集的证明编译器

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Proof-carrying code (PCC) is a technique that allows code consumers to check whether the code is safe to execute or not through a formal safety proof provided by the code producer. And a certifying compiler makes PCC practical by compiling annotated source code into low-level code and proofs. In this paper we present a certifying compiler for a subset of the C programming language, named Clike, with built-in automated theorem provers. Clike programs can be compiled by ANSI C compiler without any modification. Our compiler is intended to deal with data structures such as singly-linked lists, doubly-linked lists and trees. At the source level, we have designed a program logic combining a constrained first-order logic and a fragment of separation logic. We use a verification-condition-based method, and the generated verification conditions are sent to the built-in automated theorem prover. Our prover will generate proof terms when the input formula is valid. The low-level verification framework follows Hoare-style verification methods. The assembly code, its specification and proofs are generated automatically based on a variant of Stack-based Certifying Assembly Programming (SCAP). We implement our certifying compiler prototype in SML/NJ and build our prover libraries using the meta logic provided by Coq. We have used our prototype to successfully certify a considerable number of programs manipulating linked-lists and binary trees.
机译：携带代码（PCC）是一种技术，允许代码消费者检查代码是否安全地通过代码生产者提供的正式安全证明来执行。通过将注释的源代码编译为低级代码和校验，证明编译器使PCC实用。在本文中，我们为C编程语言的子集提供了一个证明编译器，名为CLIKE，内置自动定理普通。可以在没有任何修改的情况下由ANSI C编译器编译密码程序。我们的编译器旨在处理数据结构，例如单链接列表，双重链接列表和树木。在源级别，我们设计了一个组合受约束的一阶逻辑的程序逻辑和分离逻辑的片段。我们使用基于验证条件的方法，并将生成的验证条件发送到内置自动定论者报告。我们的箴言将在输入公式有效时生成证明术语。低级验证框架遵循Hoare式验证方法。汇编代码，其规范和证明是基于堆栈的认证组装编程（SCAP）的变体生成的。我们在SML / NJ中实现了我们的认证编译器原型，并使用COQ提供的元逻辑构建我们的先驱库。我们使用Prototype成功认证了操作链接列表和二进制树的相当数量的程序。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号