ACM SIGPLAN Notices · 2009 · 11 citations · 6 references
ComputingComputer ScienceCompilersProgramming LanguagesSoftware EngineeringAbstract Syntax TreesControl-flow AnalysisProgramming Language ImplementationStatic AnalysisStatic Code AnalysisType SystemsLanguage ImplementationLow-level C ProgrammingParser Design
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.
6
Type-safe modular hash-consing
Jean-Christophe Filliâtre, Sylvain Conchon · 2006 · 84 citations
A Value Analysis for C Programs
Géraud Canet, Pascal Cuoq, Benjamin Monate · 2009 · 67 citations
A persistent union-find data structure
Sylvain Conchon, Jean-Christophe Filliâtre · 2007 · 47 citations