Frama-C: A software analysis perspective
| LEADER | caa a22 4500 | ||
|---|---|---|---|
| 001 | 605516162 | ||
| 003 | CHVBK | ||
| 005 | 20210128100712.0 | ||
| 007 | cr unu---uuuuu | ||
| 008 | 210128e20150501xx s 000 0 eng | ||
| 024 | 7 | 0 | |a 10.1007/s00165-014-0326-7 |2 doi |
| 035 | |a (NATIONALLICENCE)springer-10.1007/s00165-014-0326-7 | ||
| 245 | 0 | 0 | |a Frama-C: A software analysis perspective |h [Elektronische Daten] |c [Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowski] |
| 520 | 3 | |a Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static analysis, deductive verification, and testing, for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements. | |
| 540 | |a British Computer Society, 2015 | ||
| 690 | 7 | |a Formal verification |2 nationallicence | |
| 690 | 7 | |a Static analysis |2 nationallicence | |
| 690 | 7 | |a Dynamic analysis |2 nationallicence | |
| 690 | 7 | |a C |2 nationallicence | |
| 700 | 1 | |a Kirchner |D Florent |u CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France |4 aut | |
| 700 | 1 | |a Kosmatov |D Nikolai |u CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France |4 aut | |
| 700 | 1 | |a Prevosto |D Virgile |u CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France |4 aut | |
| 700 | 1 | |a Signoles |D Julien |u CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France |4 aut | |
| 700 | 1 | |a Yakobowski |D Boris |u CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France |4 aut | |
| 773 | 0 | |t Formal Aspects of Computing |d Springer London |g 27/3(2015-05-01), 573-609 |x 0934-5043 |q 27:3<573 |1 2015 |2 27 |o 165 | |
| 856 | 4 | 0 | |u https://doi.org/10.1007/s00165-014-0326-7 |q text/html |z Onlinezugriff via DOI |
| 898 | |a BK010053 |b XK010053 |c XK010000 | ||
| 900 | 7 | |a Metadata rights reserved |b Springer special CC-BY-NC licence |2 nationallicence | |
| 908 | |D 1 |a research-article |2 jats | ||
| 949 | |B NATIONALLICENCE |F NATIONALLICENCE |b NL-springer | ||
| 950 | |B NATIONALLICENCE |P 856 |E 40 |u https://doi.org/10.1007/s00165-014-0326-7 |q text/html |z Onlinezugriff via DOI | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Kirchner |D Florent |u CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Kosmatov |D Nikolai |u CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Prevosto |D Virgile |u CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Signoles |D Julien |u CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Yakobowski |D Boris |u CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France |4 aut | ||
| 950 | |B NATIONALLICENCE |P 773 |E 0- |t Formal Aspects of Computing |d Springer London |g 27/3(2015-05-01), 573-609 |x 0934-5043 |q 27:3<573 |1 2015 |2 27 |o 165 | ||