@misc(FramaC,
 title        = {{Frama-C}},
 url          = {https://frama-c.com/},
)
@article(BBB2021:CACM,
 author       = {Patrick Baudin and Fran\c{c}ois Bobot and David B\"{u}hler and Lo\"{\i}c Correnson and Florent Kirchner and Nikolai Kosmatov and Andr\'{e} Maroneze and Valentin Perrelle and Virgile Prevosto and Julien Signoles and Nicky Williams},
 year         = {2021},
 title        = {The Dogged Pursuit of Bug-Free C Programs: The Frama-C Software Analysis Platform},
 journal      = {Commun. ACM},
 volume       = {64},
 number       = {8},
 pages        = {56\IeC{\textendash}68},
 doi          = {10.1145/3470569},
)
@misc(BLA2019:ZDS,
 author       = {Allan Blanchard},
 year         = {2019},
 title        = {Introduction to {C} Program Proof using {F}rama-{C} and its {WP} plugin},
 url          = {https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf},
)
@inproceedings(BKL2016:SCAM,
 author       = {Allan Blanchard and Nikolai Kosmatov and Matthieu Lemerre and Fr{\'{e}}d{\'{e}}ric Loulergue},
 year         = {2016},
 title        = {{Conc2Seq}: {A} {Frama-C} Plugin for Verification of Parallel Compositions of {C} Programs},
 booktitle    = {Int. Working Conf. on Source Code Analysis and Manipulation (SCAM'16)},
 publisher    = {{IEEE}},
 pages        = {67--72},
 doi          = {10.1109/SCAM.2016.18},
)
@inproceedings(BKL2018:HPCS,
 author       = {Allan Blanchard and Nikolai Kosmatov and Fr\'{e}d\'{e}ric Loulergue},
 year         = {2018},
 title        = {A Lesson on Verification of {IoT} Software with {F}rama-{C}},
 booktitle    = {International Conference on High Performance Computing and Simulation (HPCS)},
 publisher    = {IEEE},
 address      = {Orl\'{e}ans, France},
 pages        = {21--30},
 doi          = {10.1109/HPCS.2018.00018},
)
@inproceedings(BKL2018:SECDEV,
 author       = {Allan Blanchard and Nikolai Kosmatov and Fr\'{e}d\'{e}ric Loulergue},
 year         = {2018},
 title        = {Secure Your Things: Secure Development of {IoT} Software with {Frama-C}},
 booktitle    = {IEEE Cybersecurity Development Conference (SecDev)},
 publisher    = {IEEE},
 pages        = {126--127},
 doi          = {10.1109/SecDev.2018.00026},
)
@inproceedings(BKL2019:SAC,
 author       = {Allan Blanchard and Nikolai Kosmatov and Fr\'{e}d\'{e}ric Loulergue},
 year         = {2019},
 title        = {Logic against Ghosts: Comparison of two Proof Approaches for a List Module},
 booktitle    = {ACM Symposium on Applied Computing (SAC)},
 publisher    = {ACM},
 pages        = {2186--2195},
 doi          = {10.1145/3297280.3297495},
 note         = {Best Paper Award},
)
@inproceedings(BLK2019:NFM,
 author       = {Allan Blanchard and Fr\'{e}d\'{e}ric Loulergue and Nikolai Kosmatov},
 year         = {2019},
 title        = {{Towards Full Proof Automation in Frama-C using Auto-Active Verification}},
 booktitle    = {Nasa Formal Methods},
 series       = {LNCS},
 publisher    = {Springer},
 pages        = {88--105},
 doi          = {10.1007/978-3-030-20652-9\_6},
)
@inproceedings(2019:FMTea:Blazy,
 author       = {Sandrine Blazy},
 year         = {2019},
 title        = {{Teaching Deductive Verification in Why3 to Undergraduate Students}},
 editor       = {Brijesh Dongol and Luigia Petre and Graeme Smith},
 booktitle    = {Formal Methods Teaching},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {52--66},
 doi          = {10.1007/978-3-030-32441-4\_4},
)
@misc(ACSLbyExample,
 author       = {Jochen Burghardt and Jens Gerlach},
 year         = {2019},
 title        = {{ACSL} by Example},
 url          = {https://github.com/fraunhoferfokus/acsl-by-example},
)
@inproceedings(2019:FMTea:Leo,
 author       = {L{\'e}o Creuse and Claire Dross and Christophe Garion and J{\'e}r{\^o}me Hugues and Joffrey Huguet},
 year         = {2019},
 title        = {Teaching Deductive Verification Through Frama-C and SPARK for Non Computer Scientists},
 editor       = {Brijesh Dongol and Luigia Petre and Graeme Smith},
 booktitle    = {Formal Methods Teaching},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {23--36},
 doi          = {10.1007/s00165-014-0326-7},
)
@inproceedings(2016:CRISIS:Mangano,
 author       = {Fr{\'{e}}d{\'{e}}ric Mangano and Simon Duquennoy and Nikolai Kosmatov},
 year         = {2016},
 title        = {Formal Verification of a Memory Allocation Module of {C}ontiki with {F}rama-{C}: {A} Case Study},
 booktitle    = {Risks and Security of Internet and Systems (CRiSIS)},
 series       = {LNCS},
 volume       = {10158},
 publisher    = {Springer},
 pages        = {114--120},
 doi          = {10.1007/978-3-319-54876-0\_9},
)
@book(NN1992:WILEY,
 author       = {Hanne Riis Nielson and Flemming Nielson},
 year         = {1992},
 title        = {Semantics with applications -- a formal introduction},
 publisher    = {Wiley},
)
@conference(2016:ENSASE:Spichkova,
 author       = {Maria Spichkova. and Anna Zamansky.},
 year         = {2016},
 title        = {Teaching of Formal Methods for Software Engineering},
 booktitle    = {Proceedings of the 11th International Conference on Evaluation of Novel Software Approaches to Software Engineering - COLAFORM, (ENASE 2016)},
 organization = {INSTICC},
 publisher    = {SciTePress},
 pages        = {370--376},
 doi          = {10.5220/0005928503700376},
)