userman.bib

@manual{plugin-dev-guide,
  author = {Julien Signoles and Thibaud Antignac and Loïc Correnson and Matthieu Lemerre and
            Virgile Prevosto},
  title  = {{Frama-C Plug-in Development Guide}},
  year   = 2015,
  month  = feb,
  note   = {\newline \url{http://frama-c.com/download/frama-c-plugin-development-guide.pdf}},
}

@manual{value,
  author = {Pascal Cuoq and Boris Yakobowski and Virgile Prevosto},
  title  = {{Frama-C}'s value analysis plug-in},
  year   = 2015,
  month  = feb,
  note   = {\mbox{\url{http://frama-c.com/download/frama-c-eva-manual.pdf}}},
}

@manual{acsl,
  author = {Baudin, Patrick and Cuoq, Pascal and Filli\^{a}tre, Jean-Christophe and
            March\'{e}, Claude and Monate, Benjamin and Moy, Yannick and
            Prevosto, Virgile},
  month = nov,
  title = {{ACSL: ANSI/ISO C Specification Language. Version 1.16}},
  year = {2020}
}

@manual{acsl-implem,
  author = {Baudin, Patrick and Cuoq, Pascal and Filli\^{a}tre, Jean-Christophe and
            March\'{e}, Claude and Monate, Benjamin and Moy, Yannick and
            Prevosto, Virgile},
  month = nov,
  title = {ACSL: ANSI/ISO C Specification Language. Version 1.16 -- as implemented
  in Frama-C 22.0},
  year = {2020}
}

@misc{slicing,
  author = {Patrick Baudin and Anne Pacalet},
  title = {Slicing plug-in},
  note = {\mbox{\url{http://frama-c.com/slicing.html}}},
}

@manual{wp,
  author = {Loïc Correnson and Zaynah Dargaye and Anne Pacalet},
  title  = {{Frama-C}'s {WP} plug-in},
  year   = 2015,
  month  = feb,
  note   = {\mbox{\url{http://frama-c.com/download/frama-c-wp-manual.pdf}}},
}

@manual{rte,
  author = {Philippe Herrmann and Julien Signoles},
  title  = {Annotation Generation: {Frama-C}'s {RTE} plug-in},
  year   = 2013,
  month  = apr,
  note   = {\mbox{\url{http://frama-c.com/download/frama-c-rte-manual.pdf}}},
}

@manual{aorai,
  author = {Nicolas Stouls and Virgile Prevosto},
  title  = {{Frama-C}'s {Aora\"i} plug-in},
  year   = 2013,
  month  = apr,
  note   = {\mbox{\url{http://frama-c.com/download/frama-c-aorai-manual.pdf}}},
}

@inproceedings{fmics12,
  author = {Loïc Correnson and Julien Signoles},
  title  = {{Combining Analysis for C Program Verification}},
  booktitle = {{Formal Methods for Industrial Critical Systems (FMICS)}},
  year   = 2012,
  month  = Aug,
}

@inproceedings{sefm12,
  author = {Pascal Cuoq and Florent Kirchner and Nikolai Kosmatov and Virgile
            Prevosto and Julien Signoles and Boris Yakobowski},
  title  = {{Frama-C, A software Analysis Perspective}},
  booktitle = {{Software Engineering and Formal Methods (SEFM)}},
  year   = 2012,
  month  = oct,
}

@article{fac15,
year={2015},
journal={Formal Aspects of Computing},
title={{Frama-C}: A software analysis perspective},
publisher={Springer London},
keywords={Formal verification; Static analysis; Dynamic analysis; C},
author={Kirchner, Florent and Kosmatov, Nikolai and Prevosto, Virgile and Signoles, Julien and Yakobowski, Boris},
pages={1-37},
language={English},
note={Extended version of \cite{sefm12}},
}

@inproceedings{sac13,
  author = {M. Delahaye and N. Kosmatov and J. Signoles},
  title  = {Common Specification Language for Static and Dynamic Analysis of 
           {C} Programs},
  booktitle = {the 28th Annual ACM Symposium on Applied Computing ({SAC})},
  publisher = {ACM},
  year  = 2013,
  month = mar,
  pages = {1230--1235},
}

@manual{eacsl,
  title  = {Frama-C's E-ACSL Plug-in},
  author = {Julien Signoles and Basile Desloges and Kostyantyn Vorobyov},
  note   = {\url{https://frama-c.com/fc-plugins/e-acsl.html}},
}

@inproceedings{secureflow1,
  author = {Gerg\"o Barany and Julien Signoles},
  title  = {{Hybrid Information Flow Analysis for Real-World C Code}},
  booktitle  = {International Conference on Tests and Proofs (TAP'17)},
  year   = 2017,
  month  = jul,
}

@phdthesis{secureflow2,
  author = {Mounir Assaf},
  title  = {{From Qualitative to Quantitative Program Analysis:
 Permissive Enforcement of Secure Information Flow}},
  year   = 2015,
  month  = may,
  school = {Universit\'e Rennes 1},
}

@article{ltest,
  TITLE = {{Detection of Polluting Test Objectives for Dataflow Criteria}},
  AUTHOR = {Martin, Thibault and Kosmatov, Nikolai and Pr{\'e}vosto, Virgile and Lemerre, Matthieu},
  URL = {https://hal-cea.archives-ouvertes.fr/cea-02974228},
  NOTE = {International Conference on Integrated Formal Methods 2020-11-16/20, Lugano, Suisse},
  JOURNAL = {{Lecture Notes in Computer Science}},
  PUBLISHER = {{Springer}},
  NUMBER = {12546},
  YEAR = {2020},
  PDF = {https://hal-cea.archives-ouvertes.fr/cea-02974228/file/main.pdf},
  HAL_ID = {cea-02974228},
  HAL_VERSION = {v1},
}

@manual{mthread,
  author = {Boris Yakobowski and Richard Bonichon},
  title  = {{Frama-C}'s {Mthread} plug-in},
  year   = 2012,
  note   = {\mbox{\url{http://frama-c.com/download/frama-c-mthread-manual.pdf}}},
}

@manual{framaclang,
  author = {David Cok},
  title  = {{Frama-C}'s {Frama-Clang} plug-in},
  year   = 2021,
  note   = {\mbox{\url{https://www.frama-c.com/download/frama-clang-manual.pdf}}},
}

@inproceedings{metacsl,
  TITLE = {{MetAcsl: Specification and Verification of High-Level Properties}},
  AUTHOR = {Robles, Virgile and Kosmatov, Nikolai and Pr{\'e}vosto, Virgile and Rilling, Louis and Le Gall, Pascale},
  URL = {https://hal-cea.archives-ouvertes.fr/cea-02019790},
  BOOKTITLE = {{TACAS 2019}},
  ADDRESS = {Prague, Czech Republic},
  SERIES = {LNCS},
  VOLUME = {11427},
  YEAR = {2019},
  MONTH = Apr,
  DOI = {10.1007/978-3-030-17462-0\_22},
  KEYWORDS = {Frama-C ; meta-properties ; deductive verification ; formal specification},
  PDF = {https://hal-cea.archives-ouvertes.fr/cea-02019790/file/main.pdf},
  HAL_ID = {cea-02019790},
  HAL_VERSION = {v1},
}