Program Logics for Certified Compilers

Andrew W. Appel

  • 出版商: Cambridge
  • 出版日期: 2014-04-21
  • 售價: $3,960
  • 貴賓價: 9.5$3,762
  • 語言: 英文
  • 頁數: 472
  • 裝訂: Hardcover
  • ISBN: 110704801X
  • ISBN-13: 9781107048010
  • 相關分類: Compiler
  • 海外代購書籍(需單獨結帳)

買這商品的人也買了...

相關主題

商品描述

Separation Logic is the twenty-first-century variant of Hoare Logic that permits verification of pointer-manipulating programs. This book covers practical and theoretical aspects of Separation Logic at a level accessible to beginning graduate students interested in software verification. On the practical side it offers an introduction to verification in Hoare and Separation logics, simple case studies for toy languages, and the Verifiable C program logic for the C programming language. On the theoretical side it presents separation algebras as models of separation logics; step-indexed models of higher-order logical features for higher-order programs; indirection theory for constructing step-indexed separation algebras; tree-shares as models for shared ownership; and the semantic construction (and soundness proof) of Verifiable C. In addition, the book covers several aspects of the CompCert verified C compiler, and its connection to foundationally verified software analysis tools. All constructions and proofs are made rigorous and accessible in the Coq developments of the open-source Verified Software Toolchain.

商品描述(中文翻譯)

分離邏輯是二十一世紀的霍爾邏輯變體,允許對指標操作程序進行驗證。本書涵蓋了分離邏輯的實用和理論方面,適合對軟體驗證感興趣的初學研究生。在實用方面,它提供了霍爾邏輯和分離邏輯驗證的介紹、玩具語言的簡單案例研究,以及針對 C 程式語言的可驗證 C 程式邏輯。在理論方面,它呈現了作為分離邏輯模型的分離代數;針對高階程序的高階邏輯特徵的步驟索引模型;用於構建步驟索引分離代數的間接理論;作為共享擁有模型的樹狀共享;以及可驗證 C 的語義構造(和健全性證明)。此外,本書還涵蓋了 CompCert 驗證 C 編譯器的幾個方面,以及它與基礎驗證軟體分析工具的聯繫。所有的構造和證明都在開源的可驗證軟體工具鏈的 Coq 開發中進行了嚴謹和可及的處理。