The Dogged Pursuit of Bug-Free C Programs: The Frama-C Software Analysis Platform.
The article criticizes aspects of the computer programming language C with a focus on the use of the Frama-C26 code analysis platform to proactively address illegal programs written in C. A gallery of Frama-C26 plug-ins for varying analyses and use cases including undefined behavior, verification of...
| Publicado en: | Communications of the ACM Vol. 64; no. 8; pp. 56 - 69 |
|---|---|
| Autores principales: | , , , , , , , , , , |
| Formato: | Artículo |
| Publicado: |
Association for Computing Machinery
Aug2021
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=151620524&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 151620524 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00010782 ACM jtl: Communications of the ACM issn: 00010782 maglogo: N pubinfo: dt: Aug2021 vid: 64 iid: 8 pid: 68 pub: Association for Computing Machinery artinfo: ui: 151620524 10.1145/3470569 ppf: 56 ppct: 13 formats: tig: atl: The Dogged Pursuit of Bug-Free C Programs: The Frama-C Software Analysis Platform. aug: au: BAUDIN, PATRICK BOBOT, FRANÇOIS BÜHLER, DAVID CORRENSON, LOÏC KIRCHNER, FLORENT KOSMATOV, NIKOLAI MARONEZE, ANDRÉ PERRELLE, VALENTIN PREVOSTO, VIRGILE SIGNOLES, JULIEN WILLIAMS, NICKY affil: Researcher at the Université Paris-Saclay, CEA, List, Palaiseau, France Head of the department at the Université Paris-Saclay, CEA, List, Palaiseau, France Researcher at Thales Research and Technology, Palaiseau, France su: C (Computer program language) Programming languages Plug-ins (Computer programs) Software verification Computer programming sug: subj: C (Computer program language) Programming languages Plug-ins (Computer programs) Software verification Computer programming ab: The article criticizes aspects of the computer programming language C with a focus on the use of the Frama-C26 code analysis platform to proactively address illegal programs written in C. A gallery of Frama-C26 plug-ins for varying analyses and use cases including undefined behavior, verification of functional properties, and test case generation is provided. The use of Frama-C26 in education as well as industrial collaboration is outlined. pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2021 holdings: @attributes: islocal: N |
|---|