首页    期刊浏览 2024年11月13日 星期三
登录注册

文章基本信息

  • 标题:C floating-point proofs layered with VST and Flocq
  • 本地全文:下载
  • 作者:Andrew W. Appel ; Yves Bertot
  • 期刊名称:Journal of Formalized Reasoning
  • 印刷版ISSN:1972-5787
  • 出版年度:2021
  • 卷号:13
  • 期号:1
  • 页码:1-16
  • DOI:10.6092/issn.1972-5787/11442
  • 语种:English
  • 出版社:Alma Mater Studiorum - University of Bologna
  • 摘要:We demonstrate tools and methods for proofs about the correctness and numerical accuracy of C programs. The tools are foundational, in that they are connected to formal semantic specifications of the C operational semantics and of the IEEE 754 floating-point format. The tools are modular, in that the reasoning about C programming can be done quite separately from the reasoning about numerical correctness and numerical accuracy. The tools are general, in that they accommodate almost the entire C language (with pointer data structures, function pointers, control flow, etc.) and applied mathematics (reasoned about in a general-purpose logic and proof assistant with substantial libraries for mathematical reasoning). We demonstrate on a simple Newton's-method square root function.
国家哲学社会科学文献中心版权所有