References

  1. Frama-C. Available at https://frama-c.com/.
  2. Patrick Baudin, François Bobot, David Bühler, Loïc Correnson, Florent Kirchner, Nikolai Kosmatov, André Maroneze, Valentin Perrelle, Virgile Prevosto, Julien Signoles & Nicky Williams (2021): The Dogged Pursuit of Bug-Free C Programs: The Frama-C Software Analysis Platform. Commun. ACM 64(8), pp. 5668, doi:10.1145/3470569.
  3. Allan Blanchard (2019): Introduction to C Program Proof using Frama-C and its WP plugin. Available at https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf.
  4. Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre & Frédéric Loulergue (2016): Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs. In: Int. Working Conf. on Source Code Analysis and Manipulation (SCAM'16). IEEE, pp. 67–72, doi:10.1109/SCAM.2016.18.
  5. Allan Blanchard, Nikolai Kosmatov & Frédéric Loulergue (2018): A Lesson on Verification of IoT Software with Frama-C. In: International Conference on High Performance Computing and Simulation (HPCS). IEEE, Orléans, France, pp. 21–30, doi:10.1109/HPCS.2018.00018.
  6. Allan Blanchard, Nikolai Kosmatov & Frédéric Loulergue (2018): Secure Your Things: Secure Development of IoT Software with Frama-C. In: IEEE Cybersecurity Development Conference (SecDev). IEEE, pp. 126–127, doi:10.1109/SecDev.2018.00026.
  7. Allan Blanchard, Nikolai Kosmatov & Frédéric Loulergue (2019): Logic against Ghosts: Comparison of two Proof Approaches for a List Module. In: ACM Symposium on Applied Computing (SAC). ACM, pp. 2186–2195, doi:10.1145/3297280.3297495. Best Paper Award.
  8. Allan Blanchard, Frédéric Loulergue & Nikolai Kosmatov (2019): Towards Full Proof Automation in Frama-C using Auto-Active Verification. In: Nasa Formal Methods, LNCS. Springer, pp. 88–105, doi:10.1007/978-3-030-20652-9_6.
  9. Sandrine Blazy (2019): Teaching Deductive Verification in Why3 to Undergraduate Students. In: Brijesh Dongol, Luigia Petre & Graeme Smith: Formal Methods Teaching. Springer International Publishing, Cham, pp. 52–66, doi:10.1007/978-3-030-32441-4_4.
  10. Jochen Burghardt & Jens Gerlach (2019): ACSL by Example. Available at https://github.com/fraunhoferfokus/acsl-by-example.
  11. Léo Creuse, Claire Dross, Christophe Garion, Jérôme Hugues & Joffrey Huguet (2019): Teaching Deductive Verification Through Frama-C and SPARK for Non Computer Scientists. In: Brijesh Dongol, Luigia Petre & Graeme Smith: Formal Methods Teaching. Springer International Publishing, Cham, pp. 23–36, doi:10.1007/s00165-014-0326-7.
  12. Frédéric Mangano, Simon Duquennoy & Nikolai Kosmatov (2016): Formal Verification of a Memory Allocation Module of Contiki with Frama-C: A Case Study. In: Risks and Security of Internet and Systems (CRiSIS), LNCS 10158. Springer, pp. 114–120, doi:10.1007/978-3-319-54876-0_9.
  13. Hanne Riis Nielson & Flemming Nielson (1992): Semantics with applications – a formal introduction. Wiley.
  14. Maria Spichkova. & Anna Zamansky. (2016): Teaching of Formal Methods for Software Engineering. In: Proceedings of the 11th International Conference on Evaluation of Novel Software Approaches to Software Engineering - COLAFORM, (ENASE 2016). INSTICC. SciTePress, pp. 370–376, doi:10.5220/0005928503700376.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org