Guide to Software Verification with Frama-C: Core Components, Usages, and Applications (Frama-C 軟體驗證指南：核心組件、用法與應用)
Kosmatov, Nikolai, Prevosto, Virgile, Signoles, Julien
- 出版商: Springer
- 出版日期: 2024-07-10
- 售價: $2,960
- 貴賓價: 9.5 折 $2,812
- 語言: 英文
- 頁數: 697
- 裝訂: Hardcover - also called cloth, retail trade, or trade
- ISBN: 3031556070
- ISBN-13: 9783031556074
海外代購書籍(需單獨結帳)
相關主題
商品描述
Frama-C is a popular open-source toolset for analysis and verification of C programs, largely used for teaching, experimental research, and industrial applications.
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 是該校的研究主任。
作者簡介
Nikolai Kosmatov is a research engineer at Thales Research & Technology since 2019, where he leads the Formal Methods group. His main focus is applying formal methods based techniques and tools (including Frama-C) to industrial projects. Previously, he worked for 13 years at CEA List as an expert researcher in the Frama-C team at Software Safety and Security Lab (LSL). He obtained Ph.D. in Mathematics in 2001 from St.Petersburg State Univ., MS in Computer Science in 2003 from Univ. of Besançon, and Habilitation in Computer Science (HDR) from Univ. Paris-Sud in 2018. His research interests include software testing, formal verification, combinations between static and dynamic analysis techniques, and runtime verification. He co-authored four patents and more than 90 scientific papers in international conferences and journals. He was PC co-chair of several international events related to verification and testing, e.g., TAP 2015, IFIP-ICTSS 2019, ACM SAC-SVT 2020 and 2021. He is co-responsible for the working group on software testing (MTV2) of the French CNRS network on Programming and Software Engineering (GDR GPL) and organizes its annual workshops. Dr. Kosmatov contributed to the design and development of several software verification tools. He is the main author of the PathCrawler-online.com testing web service.
Virgile Prevosto is a researcher, senior expert in static analysis and formal methods at Université Paris-Saclay, CEA, List, where he works since 2006 in the Software Safety and Security Lab (LSL). After an engineering degree and MS in Computer Science at École Polytechnique (France), he got a Ph.D. in Computer Science from Univ. Paris 6 (now Sorbonne Université) in 2003. He has been one of the main developers of the Frama-C platform nearly since its inception and co-authored more than 25 peer-reviewed papers on Frama-C-related topics. He gave tutorials and training sessions on Frama-C in various academic and industrial venues and teaches static analysis and Frama-C for more than ten years at ENSIIE. He was a co-chair of the program committee of the Formal IDE (F-IDE) workshops in 2018 and 2019 and TAP conference in 2023. He has been CEA List's principal investigator in many collaborative projects at national and European levels, including the technical coordination of U3CAT (French ANR), Device-Soft (French/German Projet Inter Carnot Fraunhofer), and Decoder (H2020).
Julien Signoles is a research director at Université Paris-Saclay, CEA, List, where he works since 2006 in the Software Safety and Security Lab (LSL). He got a Ph.D. in Computer Science from University Paris-Sud (now University Paris-Saclay, France) in 2006 and an Habilitation (HDR) from the same university in 2018. His research focuses on runtime annotation checking and applications of formal methods to code safety and security. He is one of the main contributors to Frama-C since its conception. In particular, he is the scientific head of E-ACSL, theruntime annotation checker of Frama-C. He published more than 50 peer-reviewed papers on Frama-C-related topics. He teaches formal methods in French universities and engineering schools, and has given plenty of Frama-C tutorials and talks to a broad audience including students, academic researchers, as well as engineers and decision-makers from industry. He has been the CEA List's principal investigator in many French and European projects. He is co-responsible for the working group on Languages and Program Verification (LVP) of the French CNRS network on Programming and Software Engineering (GDR GPL) and scientific advisor of the Department of Software and System Engineering at CEA List.作者簡介(中文翻譯)
尼古拉·科斯馬托夫（Nikolai Kosmatov）自2019年起擔任泰雷茲研究與技術（Thales Research & Technology）的研究工程師，並領導形式方法小組。他的主要研究重點是將形式方法相關的技術和工具（包括Frama-C）應用於工業項目。此前，他在法國原子能與替代能源委員會（CEA List）工作了13年，擔任Frama-C團隊的專家研究員，隸屬於軟體安全與安全實驗室（Software Safety and Security Lab, LSL）。他於2001年在聖彼得堡國立大學獲得數學博士學位，2003年在貝桑松大學獲得計算機科學碩士學位，並於2018年在巴黎南大學獲得計算機科學的資格認證（Habilitation）。他的研究興趣包括軟體測試、形式驗證、靜態與動態分析技術的結合以及運行時驗證。他共同撰寫了四項專利和90多篇國際會議及期刊的科學論文。他曾擔任多個與驗證和測試相關的國際活動的程序委員會共同主席，例如TAP 2015、IFIP-ICTSS 2019、ACM SAC-SVT 2020和2021。他是法國國家科學研究中心（CNRS）編程與軟體工程網絡（GDR GPL）軟體測試工作組（MTV2）的共同負責人，並組織其年度研討會。科斯馬托夫博士參與了多個軟體驗證工具的設計與開發。他是PathCrawler-online.com測試網路服務的主要作者。
維吉爾·普雷沃斯托（Virgile Prevosto）是巴黎薩克雷大學（Université Paris-Saclay）、法國原子能與替代能源委員會（CEA）List的研究員及靜態分析和形式方法的高級專家，自2006年以來在軟體安全與安全實驗室（LSL）工作。在法國的巴黎高科（École Polytechnique）獲得工程學位和計算機科學碩士學位後，他於2003年在巴黎第六大學（現為索邦大學）獲得計算機科學博士學位。他幾乎自Frama-C平台創立以來便成為主要開發者之一，並共同撰寫了25篇以上的同行評審論文，涉及Frama-C相關主題。他在各種學術和工業場合提供Frama-C的教程和培訓課程，並在ENSIIE教授靜態分析和Frama-C超過十年。他曾擔任2018年和2019年形式IDE（F-IDE）研討會及2023年TAP會議的程序委員會共同主席。他是CEA List在許多國家和歐洲層面的合作項目的主要研究者，包括U3CAT（法國ANR）、Device-Soft（法德Inter Carnot Fraunhofer項目）和Decoder（H2020）的技術協調。
朱利安·西尼奧勒斯（Julien Signoles）是巴黎薩克雷大學（Université Paris-Saclay）、法國原子能與替代能源委員會（CEA）List的研究主任，自2006年以來在軟體安全與安全實驗室（LSL）工作。他於2006年在巴黎南大學（現為巴黎薩克雷大學）獲得計算機科學博士學位，並於2018年在同一所大學獲得資格認證（Habilitation）。他的研究重點是運行時註解檢查和形式方法在代碼安全與安全中的應用。他自Frama-C創立以來便是主要貢獻者之一，特別是他是E-ACSL的科學負責人，這是Frama-C的運行時註解檢查器。他在Frama-C相關主題上發表了50篇以上的同行評審論文。他在法國的各大學和工程學院教授形式方法，並向包括學生、學術研究人員以及來自工業界的工程師和決策者等廣泛受眾提供了多場Frama-C的教程和演講。他是CEA List在許多法國和歐洲項目的主要研究者。他是法國國家科學研究中心（CNRS）編程與軟體工程網絡（GDR GPL）語言與程序驗證工作組（LVP）的共同負責人，並擔任CEA List軟體與系統工程部的科學顧問。
