LEADER 01801cam0-22005291i-450- 001 990000838700403321 005 20060608144336.0 035 $a000083870 035 $aFED01000083870 035 $a(Aleph)000083870FED01 035 $a000083870 100 $a20020821d1964----km-y0itay50------ba 101 0 $aeng 105 $ay-------001yy 200 1 $a<>course of higher mathematics$fV. I. Smirnov 210 $aOxford$cPergamon Press$d1964 215 $a5 v. in 6$d23 cm 225 1 $aInternational series of monographs on pure and applied mathematics 327 1 $a1.: Elementary calculus$a2.: Advanced calculus$a3.1: Linear algebra$a3.2: Complex variables special functions$a4.: Integral equations and partial differential Equations$a5.: Integration and functional analysis 610 0 $aAnalisi funzionale 676 $a515 700 1$aSmirnov,$bVladimir Ivanovic$028667 801 0$aIT$bUNINA$gRICA$2UNIMARC 901 $aBK 912 $a990000838700403321 952 $a02 6 A 12$b1859$fFINBN 952 $a02 6 A 1$b1742$fFINBN 952 $a02 6 A 4$b1739$fFINBN 952 $a02 6 A 3$b1740$fFINBN 952 $a02 6 A 15$b1823$fFINBN 952 $a02 6 A 13$b1860$fFINBN 952 $a02 6 A 11$b1858$fFINBN 952 $a02 6 A 10$b1857$fFINBN 952 $a02 6 A 6$b1737$fFINBN 952 $a02 6 A 5$b1738$fFINBN 952 $a02 6 A 2$b1741$fFINBN 952 $a02 6 A 14$b1861$fFINBN 952 $a09 006-030/1$b2359$fDINAE 952 $a09 006-030/3.1$b2361$fDINAE 952 $a09 006-030/3.2$b2362$fDINAE 952 $a09 006-030/4$b2363$fDINAE 952 $a09 006-030/5$b2364$fDINAE 952 $a09 006-030/2$b2360$fDINAE 959 $aFINBN 959 $aDINAE 996 $aCourse of higher mathematics$9347967 997 $aUNINA LEADER 05156nam 22006735 450 001 9910872183403321 005 20240827194729.0 010 $a3-031-55608-9 024 7 $a10.1007/978-3-031-55608-1 035 $a(CKB)32775674000041 035 $a(MiAaPQ)EBC31523162 035 $a(Au-PeEL)EBL31523162 035 $a(DE-He213)978-3-031-55608-1 035 $a(OCoLC)1446801037 035 $a(EXLCZ)9932775674000041 100 $a20240709d2024 u| 0 101 0 $aeng 135 $aur||||||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aGuide to Software Verification with Frama-C $eCore Components, Usages, and Applications /$fedited by Nikolai Kosmatov, Virgile Prevosto, Julien Signoles 205 $a1st ed. 2024. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2024. 215 $a1 online resource (708 pages) 225 1 $aComputer Science Foundations and Applied Logic,$x2731-5762 311 08$a3-031-55607-0 327 $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. 330 $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. 410 0$aComputer Science Foundations and Applied Logic,$x2731-5762 606 $aComputer programs$xTesting 606 $aProgramming languages (Electronic computers) 606 $aMathematics$xData processing 606 $aCoding theory 606 $aInformation theory 606 $aSoftware Testing 606 $aProgramming Language 606 $aComputational Mathematics and Numerical Analysis 606 $aCoding and Information Theory 615 0$aComputer programs$xTesting. 615 0$aProgramming languages (Electronic computers) 615 0$aMathematics$xData processing. 615 0$aCoding theory. 615 0$aInformation theory. 615 14$aSoftware Testing. 615 24$aProgramming Language. 615 24$aComputational Mathematics and Numerical Analysis. 615 24$aCoding and Information Theory. 676 $a005.14 700 $aKosmatov$b Nikolai$01744495 701 $aPrevosto$b Virgile$01378504 701 $aSignoles$b Julien$01744496 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910872183403321 996 $aGuide to Software Verification with Frama-C$94174479 997 $aUNINA