More Web Proxy on the site http://driver.im/

research-article

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

Authors:

Julien Signoles,

Patrick Baudin,

Richard Bonichon,

Loïc Correnson,

Benjamin Monate,

Virgile Prevosto,

Armand PuccettiAuthors Info & Claims

ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming

Pages 281 - 286

https://doi.org/10.1145/1596550.1596591

Published: 31 August 2009 Publication History

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.

Supplementary Material

JPG File (experiencereportocamlforanindustrial-strengthstaticanalysis.jpg)

Download
15.15 KB

MP4 File (experiencereportocamlforanindustrial-strengthstaticanalysis.mp4)

Download
78.50 MB

References

[1]

Patrick Baudin, Anne Pacalet, Jacques Raguideau, Dominique Schoen, and Nicky Williams. Caveat: a tool for software validation. In phDependable Systems and Networks, 2002, pages 537, 2002.

Digital Library

[2]

Patrick Baudin, Jean-Christophe Filliâtre, Thierry Hubert, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. phACSL: ANSI C Specification Language (preliminary design V1.4), preliminary edition, October 2008. URL http://frama-c.cea.fr/acsl.html.

[3]

Géraud Canet, Pascal Cuoq, and Benjamin Monate. A value analysis for C programs, 2009. To appear in the proceedings of SCAM2009.

Digital Library

[4]

Sylvain Conchon and Jean-Christophe Filliâtre. A persistent union-find data structure. In ML '07: Proceedings of the 2007 workshop on Workshop on ML, pages 37--46, New York, NY, USA, 2007. ACM. ISBN 978-1-59593-676-9. http://doi.acm.org/10.1145/1292535.1292541.

Digital Library

[5]

Sylvain Conchon, Jean--Christophe Filliâtre, and Julien Signoles. Designing a generic graph library using ML functors. In Marco T. Morazán, editor, Trends in Functional Programming, volume 8 of phTrends in Functional Programming, pages 124--140. Intellect, UK/The University of Chicago Press, USA, 2008. ISBN 978-1-84150-196-3.

[6]

Pascal Cuoq. Documentation of Frama-C's value analysis plug-in, 2008. URL http://frama-c.cea.fr/download/frama-c-manual-Lithium-en.pdf.

[7]

Pascal Cuoq and Damien Doligez. Hashconsing in an incrementally garbage-collected system: a story of weak pointers and hashconsing in OCaml 3.10.2. In ML '08: Proceedings of the 2008 ACM SIGPLAN workshop on ML, pages 13--22, New York, NY, USA, 2008. ACM. ISBN 978-1-60558-062-3.

Digital Library

[8]

David Delmas, Stéphane Duprat, Patrick Baudin, and Benjamin Monate. Proving temporal properties at code level for basic operators of control/command programs. In ph4th European Congress on Embedded Real Time Software, 2008.

[9]

Jean-Christophe Filliâtre and Sylvain Conchon. Type-safe modular hash-consing. In ML '06: Proceedings of the 2006 workshop on ML, pages 12--19, New York, NY, USA, 2006. ACM. ISBN 1-59593-483-9.

Digital Library

[10]

Xavier Leroy. A syntactic theory of type generativity and sharing. Journal of Functional Programming, 6: 1--32, 1996.

[11]

Yaron Minsky. Caml trading: Experiences in functional programming on Wall Street. In Wouter Swierstra, editor, The Monad. Reader, April 2007.

[12]

Benjamin Monate and Julien Signoles. Slicing for security of code. In Peter Lipp, Ahmad-Reza Sadeghi, and Klaus-Michael Koch, editors, phTRUST, volume 4968 of Lecture Notes in Computer Science, pages 133--142. Springer-Verlags, March 2008.

Digital Library

[13]

Ravi Nanavati. Experience report: a pure shirt fits. SIGPLAN Not., 43 (9): 347--352, 2008. ISSN 0362-1340.

Digital Library

[14]

George C. Necula, Scott Mcpeak, Shree P. Rahul, and Westley Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In International Conference on Compiler Construction, pages 213--228, 2002.

Digital Library

[15]

Famantanantsoa Randimbivololona, Jean Souyris, Patrick Baudin, Anne Pacalet, Jacques Raguideau, and Dominique Schoen. Applying formal proof techniques to avionics software: A pragmatic approach. In FM '99: Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume II, pages 1798--1815, London, UK, 1999. Springer-Verlag. ISBN 3-540-66588-9.

Digital Library

[16]

Morten Rhiger. A foundation for embedded languages. ACM Transactions on Programming Languages and Systems (TOPLAS), 25 (3): 291--315, 2003. ISSN 0164-0925.

Digital Library

[17]

Julien Signoles. Plug-in development guide, 2008. URL http://frama-c.cea.fr/download/plug-in_development_guide.pdf.

[18]

Julien Signoles. Foncteurs impératifs et composés: la notion de projets dans Frama-C. In Actes des Journées Francophones des Langages Applicatifs, pages 37--54, January 2009. In French.

Cited By

Bobot FMaroneze APrevosto VSignoles J(2024)The Art of Developing Frama-C Plug-insGuide to Software Verification with Frama-C10.1007/978-3-031-55608-1_7(341-401)Online publication date: 10-Jul-2024
https://doi.org/10.1007/978-3-031-55608-1_7
Maroneze APrevosto VSignoles J(2024)The Heart of Frama-C: The Frama-C KernelGuide to Software Verification with Frama-C10.1007/978-3-031-55608-1_2(81-130)Online publication date: 10-Jul-2024
https://doi.org/10.1007/978-3-031-55608-1_2
Keyes OPeil BWilliams RSpiel K(2020)Reimagining (Women’s) HealthACM Transactions on Computer-Human Interaction10.1145/340421827:4(1-42)Online publication date: 26-Aug-2020
https://dl.acm.org/doi/10.1145/3404218
Show More Cited By

Index Terms

Experience report: OCaml for an industrial-strength static analysis framework
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages

Recommendations

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

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 ...
Modular language implementation in Rascal - experience report

All software evolves, and programming languages and programming language tools are no exception. And just like in ordinary software construction, modular implementations can help ease the process of changing a language implementation and its dependent ...
Compiling Embedded Programs to Byte Code
PADL '02: Proceedings of the 4th International Symposium on Practical Aspects of Declarative Languages

Functional languages have proven substantially useful for hosting embedded domain-specific languages. They provide an infrastructure rich enough to define both a convenient syntax for the embedded language, a type system for embedded programs, and an ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming

August 2009

364 pages

ISBN:9781605583327

DOI:10.1145/1596550

General Chair:
Graham Hutton
University of Nottingham
,
Program Chair:
Andrew Tolmach
Portland State University

ACM SIGPLAN Notices Volume 44, Issue 9
ICFP '09
September 2009
343 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1631687
Issue’s Table of Contents

Copyright © 2009 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 31 August 2009

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP '09

Sponsor:

ICFP '09: ACM SIGPLAN International Conference on Functional Programming

August 31 - September 2, 2009

Edinburgh, Scotland

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

43
Total Citations
View Citations
688
Total Downloads

Downloads (Last 12 months)19
Downloads (Last 6 weeks)2

Reflects downloads up to 28 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Bobot FMaroneze APrevosto VSignoles J(2024)The Art of Developing Frama-C Plug-insGuide to Software Verification with Frama-C10.1007/978-3-031-55608-1_7(341-401)Online publication date: 10-Jul-2024
https://doi.org/10.1007/978-3-031-55608-1_7
Maroneze APrevosto VSignoles J(2024)The Heart of Frama-C: The Frama-C KernelGuide to Software Verification with Frama-C10.1007/978-3-031-55608-1_2(81-130)Online publication date: 10-Jul-2024
https://doi.org/10.1007/978-3-031-55608-1_2
Keyes OPeil BWilliams RSpiel K(2020)Reimagining (Women’s) HealthACM Transactions on Computer-Human Interaction10.1145/340421827:4(1-42)Online publication date: 26-Aug-2020
https://dl.acm.org/doi/10.1145/3404218
Gerasimov A(2018)Directed Dynamic Symbolic Execution for Static Analysis Warnings ConfirmationProgramming and Computing Software10.1134/S036176881805002X44:5(316-323)Online publication date: 1-Sep-2018
https://dl.acm.org/doi/10.1134/S036176881805002X
Midtgaard JMøller A(2017)QuickChecking static analysis propertiesSoftware Testing, Verification and Reliability10.1002/stvr.164027:6Online publication date: 30-Aug-2017
https://doi.org/10.1002/stvr.1640
Kosmatov NSignoles J(2016)Frama-C, A Collaborative Framework for C Code Verification: Tutorial SynopsisRuntime Verification10.1007/978-3-319-46982-9_7(92-115)Online publication date: 20-Sep-2016
https://doi.org/10.1007/978-3-319-46982-9_7
Tang HLan THao DZhang LMei HLü JMa XWang QYin GLiao X(2015)Enhancing Defect Prediction with Static Defect AnalysisProceedings of the 7th Asia-Pacific Symposium on Internetware10.1145/2875913.2875922(43-51)Online publication date: 6-Nov-2015
https://dl.acm.org/doi/10.1145/2875913.2875922
Hennes DJong STuyls KGal Y(2015)Metastrategies in Large-Scale Bargaining SettingsACM Transactions on Intelligent Systems and Technology10.1145/27742247:1(1-23)Online publication date: 1-Oct-2015
https://dl.acm.org/doi/10.1145/2774224
Groves WGini M(2015)On Optimizing Airline Ticket Purchase TimingACM Transactions on Intelligent Systems and Technology10.1145/27333847:1(1-28)Online publication date: 1-Oct-2015
https://dl.acm.org/doi/10.1145/2733384
Midtgaard JMoller A(2015)QuickChecking Static Analysis Properties2015 IEEE 8th International Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST.2015.7102603(1-10)Online publication date: May-2015
https://doi.org/10.1109/ICST.2015.7102603
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten