000 05350nam a22006015i 4500
001 978-3-031-55608-1
003 DE-He213
005 20240730172733.0
007 cr nn 008mamaa
008 240709s2024 sz | s |||| 0|eng d
020 _a9783031556081
_9978-3-031-55608-1
024 7 _a10.1007/978-3-031-55608-1
_2doi
050 4 _aQA76.76.T48
072 7 _aUMZT
_2bicssc
072 7 _aCOM051330
_2bisacsh
072 7 _aUMZT
_2thema
082 0 4 _a005.14
_223
245 1 0 _aGuide to Software Verification with Frama-C
_h[electronic resource] :
_bCore Components, Usages, and Applications /
_cedited by Nikolai Kosmatov, Virgile Prevosto, Julien Signoles.
250 _a1st ed. 2024.
264 1 _aCham :
_bSpringer International Publishing :
_bImprint: Springer,
_c2024.
300 _aXXIV, 697 p. 196 illus., 69 illus. in color.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aComputer Science Foundations and Applied Logic,
_x2731-5762
505 0 _aForeword -- 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 _aFrama-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 _aComputer programs
_xTesting.
_980793
650 0 _aProgramming languages (Electronic computers).
_97503
650 0 _aMathematics
_xData processing.
_919904
650 0 _aCoding theory.
_94154
650 0 _aInformation theory.
_914256
650 1 4 _aSoftware Testing.
_980795
650 2 4 _aProgramming Language.
_939403
650 2 4 _aComputational Mathematics and Numerical Analysis.
_931598
650 2 4 _aCoding and Information Theory.
_9105270
700 1 _aKosmatov, Nikolai.
_eeditor.
_0(orcid)
_10000-0003-1557-2813
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9105272
700 1 _aPrevosto, Virgile.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9105273
700 1 _aSignoles, Julien.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9105275
710 2 _aSpringerLink (Online service)
_9105276
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783031556074
776 0 8 _iPrinted edition:
_z9783031556098
776 0 8 _iPrinted edition:
_z9783031556104
830 0 _aComputer Science Foundations and Applied Logic,
_x2731-5762
_9105278
856 4 0 _uhttps://doi.org/10.1007/978-3-031-55608-1
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
942 _cEBK
999 _c88520
_d88520