caa a22 4500 605516162 CHVBK 20210128100712.0 cr unu---uuuuu 210128e20150501xx s 000 0 eng 10.1007/s00165-014-0326-7 doi (NATIONALLICENCE)springer-10.1007/s00165-014-0326-7 Frama-C: A software analysis perspective [Elektronische Daten] [Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowski] 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. British Computer Society, 2015 Formal verification nationallicence Static analysis nationallicence Dynamic analysis nationallicence C nationallicence Kirchner Florent CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France aut Kosmatov Nikolai CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France aut Prevosto Virgile CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France aut Signoles Julien CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France aut Yakobowski Boris CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France aut Formal Aspects of Computing Springer London 27/3(2015-05-01), 573-609 0934-5043 27:3<573 2015 27 165 https://doi.org/10.1007/s00165-014-0326-7 text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-014-0326-7 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Kirchner Florent CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France aut NATIONALLICENCE 700 1- Kosmatov Nikolai CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France aut NATIONALLICENCE 700 1- Prevosto Virgile CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France aut NATIONALLICENCE 700 1- Signoles Julien CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France aut NATIONALLICENCE 700 1- Yakobowski Boris CEA, LIST, Software Reliability Laboratory, F-91191, Gif-sur-Yvette, France aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/3(2015-05-01), 573-609 0934-5043 27:3<573 2015 27 165