Guide to Software Verification with Frama-C: Core Components, Usages, and Applications
暫譯: Frama-C 軟體驗證指南：核心組件、用法與應用
Kosmatov, Nikolai, Prevosto, Virgile, Signoles, Julien
相關主題
商品描述
Frama-C is a popular open-source toolset for analysis and verification of C programs, largely used for teaching, experimental research, and industrial applications.
With the growing complexity and ubiquity of modern software, there is increasing interest in code analysis tools at various levels of formalization to ensure safety and security of software products. Acknowledging the fact that no single technique will ever be able to fit all software verification needs, the Frama-C platform features a wide set of plug-ins that can be used or combined for solving specific verification tasks.
This guidebook presents a large panorama of basic usages, research results, and concrete applications of Frama-C since the very first open-source release of the platform in 2008. It covers the ACSL specification language, core verification plug-ins, advanced analyses and their combinations, key ingredients for developing new plug-ins, as well as successful industrial case studies in which Frama-C has helped engineers verify crucial safety or security properties.
Topics and features:
* Gentle, example-based introduction to software specification and verification
* Wide panorama of state-of-the-art specification and analysis techniques
* Step-by-step guide to develop your own, tailor-made analysis on top of the platform
* Inspiring success stories of Frama-C deployment on industrial code
* More than 15 years of R&D on analysis and verification of C code
This book is firmly rooted on the practice of software analysis, with numerous examples, exercises and application guidelines. As such, it is particularly well suited for software verification practitioners wishing to deploy verification on their code, as well as for undergraduate students with little or no experience in code analysis techniques. More advanced sections on the theoretical underpinnings of the analyzers will be of interest for graduate students and researchers.
Nikolai Kosmatov is a Senior Researcher at Thales Research & Technology, France. Virgile Prevosto is a Senior Researcher and Julien Signoles is a Research Director, both at Université Paris-Saclay, CEA, List, France.
商品描述(中文翻譯)
Frama-C 是一個流行的開源工具集，用於分析和驗證 C 程式，廣泛應用於教學、實驗研究和工業應用。
隨著現代軟體的複雜性和普及性日益增加，對於各種形式化程度的程式碼分析工具的興趣也在上升，以確保軟體產品的安全性和可靠性。考慮到沒有任何單一技術能夠滿足所有軟體驗證需求，Frama-C 平台提供了一系列可用或可組合的插件，以解決特定的驗證任務。
本指南提供了 Frama-C 自 2008 年首次開源發布以來的基本用法、研究成果和具體應用的廣泛概覽。內容涵蓋了 ACSL 規範語言、核心驗證插件、高級分析及其組合、開發新插件的關鍵要素，以及 Frama-C 幫助工程師驗證關鍵安全或安全性屬性的成功工業案例研究。
主題和特點：
* 溫和的、基於範例的軟體規範和驗證介紹
* 最先進的規範和分析技術的廣泛概覽
* 逐步指南，幫助您在平台上開發自定義的分析
* Frama-C 在工業程式碼部署的成功故事
* 超過 15 年的 C 程式碼分析和驗證的研發經驗
本書深植於軟體分析的實踐中，包含大量範例、練習和應用指南。因此，特別適合希望在其程式碼上部署驗證的軟體驗證實踐者，以及對程式碼分析技術幾乎沒有經驗的本科生。對於研究生和研究人員來說，關於分析器理論基礎的更高級部分將會引起他們的興趣。
Nikolai Kosmatov 是法國 Thales Research & Technology 的高級研究員。Virgile Prevosto 是法國巴黎薩克雷大學 CEA List 的高級研究員，Julien Signoles 是該校的研究主任。
