Experience report: OCaml for an industrial-strength static analysis framework

Pascal Cuoq; Julien Signoles; Patrick Baudin; Richard Bonichon; Géraud Canet; Liïc Correnson; Benjamin Monate; Virgile Prevosto; Armand Puccetti

Experience report: OCaml for an industrial-strength static analysis framework

Pascal Cuoq
, Julien Signoles
, Patrick Baudin
, Richard Bonichon
, Géraud Canet
, Liïc Correnson
, Benjamin Monate
, Virgile Prevosto
, Armand Puccetti

LIST-DTSI-SLA CEA

Research output: Contribution to journal › Article › peer-review

Abstract

This experience report describes the choice of OCaml as the implementation language for Frama-C, a framework for the static analysis of C programs. OCaml became the implementation language for Frama-C because it is expressive. Most of the reasons listed in the remaining of this article are secondary reasons, features which are not specific to OCaml (modularity, availability of a C parser, control over the use of resources. . . ) but could have prevented the use of OCaml for this project if they had been missing.

Original language	English
Pages (from-to)	281-286
Number of pages	6
Journal	ACM SIGPLAN Notices
Volume	44
Issue number	9
Publication status	Published - 1 Sept 2009
Externally published	Yes

Keywords

Design
Languages
Verification

Cite this

@article{5df363347c3f4e82b594da727fa66eaa,

title = "Experience report: OCaml for an industrial-strength static analysis framework",

abstract = "This experience report describes the choice of OCaml as the implementation language for Frama-C, a framework for the static analysis of C programs. OCaml became the implementation language for Frama-C because it is expressive. Most of the reasons listed in the remaining of this article are secondary reasons, features which are not specific to OCaml (modularity, availability of a C parser, control over the use of resources. . . ) but could have prevented the use of OCaml for this project if they had been missing.",

keywords = "Design, Languages, Verification",

author = "Pascal Cuoq and Julien Signoles and Patrick Baudin and Richard Bonichon and G{\'e}raud Canet and Li{\"i}c Correnson and Benjamin Monate and Virgile Prevosto and Armand Puccetti",

year = "2009",

month = sep,

day = "1",

language = "English",

volume = "44",

pages = "281--286",

journal = "ACM SIGPLAN Notices",

issn = "1523-2867",

number = "9",

}

TY - JOUR

T1 - Experience report

T2 - OCaml for an industrial-strength static analysis framework

AU - Cuoq, Pascal

AU - Signoles, Julien

AU - Baudin, Patrick

AU - Bonichon, Richard

AU - Canet, Géraud

AU - Correnson, Liïc

AU - Monate, Benjamin

AU - Prevosto, Virgile

AU - Puccetti, Armand

PY - 2009/9/1

Y1 - 2009/9/1

N2 - This experience report describes the choice of OCaml as the implementation language for Frama-C, a framework for the static analysis of C programs. OCaml became the implementation language for Frama-C because it is expressive. Most of the reasons listed in the remaining of this article are secondary reasons, features which are not specific to OCaml (modularity, availability of a C parser, control over the use of resources. . . ) but could have prevented the use of OCaml for this project if they had been missing.

AB - This experience report describes the choice of OCaml as the implementation language for Frama-C, a framework for the static analysis of C programs. OCaml became the implementation language for Frama-C because it is expressive. Most of the reasons listed in the remaining of this article are secondary reasons, features which are not specific to OCaml (modularity, availability of a C parser, control over the use of resources. . . ) but could have prevented the use of OCaml for this project if they had been missing.

KW - Design

KW - Languages

KW - Verification

UR - https://www.scopus.com/pages/publications/70350442621

M3 - Article

AN - SCOPUS:70350442621

SN - 1523-2867

VL - 44

SP - 281

EP - 286

JO - ACM SIGPLAN Notices

JF - ACM SIGPLAN Notices

IS - 9

ER -

Experience report: OCaml for an industrial-strength static analysis framework

Abstract

Keywords

Other files and links

Fingerprint

Cite this