CoMeMoV

Collaborative Memory Models for formal Verification

Home | News | Jobs | Publications | Work Packages | Deliverables |

International conferences

  1. Virgile Robles, Nikolai Kosmatov, Virgile Prevosto and Pascale Le Gall. High-Level Program Properties in Frama-C: Definition, Verification and Deduction. In International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA), LNCS, Springer, 2024, paper
  2. Allan Blanchard, Loïc Correnson, Adel Djoudi and Nikolai Kosmatov. No Smoke without Fire: Detecting Specification Inconsistencies with Frama-C/WP. In Tests and Proofs (TAP), LNCS. Springer, 2024, paper
  3. Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, and Daniel Gracia Pérez. Runtime Verification for High-Level Security Properties: Case Study on the TPM Software Stack. In Tests and Proofs (TAP), LNCS. Springer, 2024, paper
  4. Loïc Correnson, Allan Blanchard, Adel Djoudi, Nikolai Kosmatov. Automate where Automation Fails: Proof Strategies for Frama-C/WP. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Luxembourg, LNCS 14570, Springer, 2024, paper (open access).
  5. Téo Bernier, Yani Ziani, Nikolai Kosmatov, and Frédéric Loulergue. Combining Deductive Verification with Shape Analysis. In 27th International Conference on Fundamental Approaches to Software Engineering (FASE), Luxembourg, LNCS 14573, Springer, 2024, paper (open access).
  6. Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez, and Téo Bernier. Towards Formal Verification of a TPM Software Stack. In 18th International Conference on integrated Formal Methods (iFM), LNCS 14300. Springer, 2023, preprint, paper.

National conferences

  1. Jérémy Damour, Allan Blanchard, Loïc Correnson, Frédéric Loulergue, Formalisation d’une analyse de région pour Frama-C/WP, In Journées Francophones des Langages Applicatifs (JFLA), Jan 2025, lieu-dit Saint Hilaire, Roiffé, France, to appear
  2. Téo Bernier, Yani Ziani, Nikolai Kosmatov, and Frédéric Loulergue. Combiner la vérification déductive avec l’analyse de forme. Journées Journées Approches Formelles pour l’Assistance au Développement de Logiciels (AFADL), Strasbourg, Juin 2024, résumé.