Guide to Software Verification with Frama-C (Record no. 61440)
[ view plain ]
| 000 -LEADER | |
|---|---|
| fixed length control field | 05408nam a22006015i 4500 |
| 001 - CONTROL NUMBER | |
| control field | 978-3-031-55608-1 |
| 003 - CONTROL NUMBER IDENTIFIER | |
| control field | DE-He213 |
| 005 - DATE AND TIME OF LATEST TRANSACTION | |
| control field | 20251030112619.0 |
| 007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION | |
| fixed length control field | cr nn 008mamaa |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION | |
| fixed length control field | 240709s2024 sz | s |||| 0|eng d |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| International Standard Book Number | 9783031556081 |
| -- | 978-3-031-55608-1 |
| 024 7# - OTHER STANDARD IDENTIFIER | |
| Standard number or code | 10.1007/978-3-031-55608-1 |
| Source of number or code | doi |
| 050 #4 - LIBRARY OF CONGRESS CALL NUMBER | |
| Classification number | QA76.76.T48 |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | UMZT |
| Source | bicssc |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | COM051330 |
| Source | bisacsh |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | UMZT |
| Source | thema |
| 245 10 - TITLE STATEMENT | |
| Title | Guide to Software Verification with Frama-C |
| Medium | [electronic resource] : |
| Remainder of title | Core Components, Usages, and Applications / |
| Statement of responsibility, etc. | edited by Nikolai Kosmatov, Virgile Prevosto, Julien Signoles. |
| 250 ## - EDITION STATEMENT | |
| Edition statement | 1st ed. 2024. |
| 264 #1 - PRODUCTION, PUBLICATION, DISTRIBUTION, MANUFACTURE, AND COPYRIGHT NOTICE | |
| Place of production, publication, distribution, manufacture | Cham : |
| Name of producer, publisher, distributor, manufacturer | Springer International Publishing : |
| -- | Imprint: Springer, |
| Date of production, publication, distribution, manufacture, or copyright notice | 2024. |
| 300 ## - PHYSICAL DESCRIPTION | |
| Extent | XXIV, 697 p. 196 illus., 69 illus. in color. |
| Other physical details | online resource. |
| 336 ## - CONTENT TYPE | |
| Content type term | text |
| Content type code | txt |
| Source | rdacontent |
| 337 ## - MEDIA TYPE | |
| Media type term | computer |
| Media type code | c |
| Source | rdamedia |
| 338 ## - CARRIER TYPE | |
| Carrier type term | online resource |
| Carrier type code | cr |
| Source | rdacarrier |
| 347 ## - DIGITAL FILE CHARACTERISTICS | |
| File type | text file |
| Encoding format | |
| Source | rda |
| 490 1# - SERIES STATEMENT | |
| Series statement | Computer Science Foundations and Applied Logic, |
| International Standard Serial Number | 2731-5762 |
| 505 0# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | Foreword -- Part I. Core Components -- ACSL Specification Language -- The Kernel and its Services -- Abstract Interpretation with Eva -- Deductive Verification with WP -- Runtime Assertion Checking with E-ACSL -- Test generation with PathCrawler -- Development of new plug-ins -- Part II. Advanced Usages and Combinations -- Tools for Program Understanding -- Combinations of Analyses -- Numerical Accuracy Analysis -- Analyses of Concurrent Programs -- High-Level Properties -- Part III. Applications and Emerging Domains -- Applications in Transportation, Energy and Defence -- Applications in Cybersecurity and Trusted AI -- Artificial Intelligence for Improving Verification Techniques -- Index -- Bibliography. |
| 520 ## - SUMMARY, ETC. | |
| Summary, etc. | 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. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | |
| General subdivision | Testing. |
| 9 (RLIN) | 67452 |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | |
| 9 (RLIN) | 66206 |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | |
| General subdivision | Data processing. |
| 9 (RLIN) | 65715 |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | |
| 9 (RLIN) | 65513 |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | |
| 9 (RLIN) | 57783 |
| 650 14 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | |
| 9 (RLIN) | 67454 |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | |
| 9 (RLIN) | 66208 |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | |
| 9 (RLIN) | 66073 |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | |
| 9 (RLIN) | 65515 |
| 700 1# - ADDED ENTRY--PERSONAL NAME | |
| Personal name | Kosmatov, Nikolai. |
| Relator term | editor. |
| Authority record control number | (orcid)0000-0003-1557-2813 |
| -- | https://orcid.org/0000-0003-1557-2813 |
| Relator code | edt |
| -- | http://id.loc.gov/vocabulary/relators/edt |
| 9 (RLIN) | 80222 |
| 700 1# - ADDED ENTRY--PERSONAL NAME | |
| Personal name | Prevosto, Virgile. |
| Relator term | editor. |
| Relator code | edt |
| -- | http://id.loc.gov/vocabulary/relators/edt |
| 9 (RLIN) | 80223 |
| 700 1# - ADDED ENTRY--PERSONAL NAME | |
| Personal name | Signoles, Julien. |
| Relator term | editor. |
| Relator code | edt |
| -- | http://id.loc.gov/vocabulary/relators/edt |
| 9 (RLIN) | 80224 |
| 710 2# - ADDED ENTRY--CORPORATE NAME | |
| Corporate name or jurisdiction name as entry element | SpringerLink (Online service) |
| 773 0# - HOST ITEM ENTRY | |
| Title | Springer Nature eBook |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY | |
| Relationship information | Printed edition: |
| International Standard Book Number | 9783031556074 |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY | |
| Relationship information | Printed edition: |
| International Standard Book Number | 9783031556098 |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY | |
| Relationship information | Printed edition: |
| International Standard Book Number | 9783031556104 |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE | |
| Uniform title | Computer Science Foundations and Applied Logic, |
| International Standard Serial Number | 2731-5762 |
| 9 (RLIN) | 69816 |
| 856 40 - ELECTRONIC LOCATION AND ACCESS | |
| Uniform Resource Identifier | <a href="https://doi.org/10.1007/978-3-031-55608-1">https://doi.org/10.1007/978-3-031-55608-1</a> |
| 912 ## - | |
| -- | ZDB-2-SCS |
| 912 ## - | |
| -- | ZDB-2-SXCS |
No items available.