Nikolai Kosmatov's homepage

Nikolai KOSMATOV

Researcher at Thales Research and Technology
Invited Researcher at CEA List

Mail: Nikolai Kosmatov
Thales Research and Technology
GrSTI, LSEC
1 Av. Augustin Fresnel
91120 Palaiseau
FRANCE

Email: NikolaiKosmatov(at) gmail(dot)com

Research

My current research interests include software verification, combined static and dynamic analysis, constraint solving and constraint based software testing.

Patents and Publications

Tutorials

10 October, 2019, Tutorial Formal Verification of IoT Software with Frama-C (co-organized with Allan Blanchard and Frédéric Loulergue) at FM 2019, [slides], [VM with exercises]
3 April 2019, Invited Tutorial Advanced Test Coverage Criteria: Specify and Measure, Cover and Unmask at TestCon 2019 in Moscow, Russia, [slides]
8 April, 2019, Tutorial Formal Verification for an Internet of Secured Things (co-organized with Allan Blanchard and Frédéric Loulergue) at SAC 2019, [slides], [VM with exercises]
Janvier 22, 2019, Master Class Cybersecurity and Internet of Things: Verify Your Code Today! (co-organized with Allan Blanchard) at FIC 2019, [slides]
16 October, 2018, Tutorial Towards Reliable Things: Formal Verification of IoT Software with Frama-C (co-organized with Allan Blanchard and Frédéric Loulergue) at ISSRE 2018
30 September, 2018, Tutorial Secure Your Things: Secure Development of IoT Software with Frama-C (co-organized with Allan Blanchard and Frédéric Loulergue) at SecDev 2018, [slides], [VM with exercises]
16 July 2018, Tutorial Secure Your Things: Verification of IoT Software with Frama-C (co-organized with Allan Blanchard and Frédéric Loulergue) at HPCS 2018, [slides], [VM with exercises]
28 June 2018, Tutorial Specify and Measure, Cover and Unmask: A Proof-Friendly View of Advanced Test Coverage Criteria (co-organized with Sébastien Bardin) at TAP 2018, [slides]
30 May 2018, Tutorial Towards Secure Things, or How to Verify IoT Software with Frama-C (co-organized with Allan Blanchard and Frédéric Loulergue) at ZINC 2018, [slides], [VM with exercises]
20 March 2018, Tutorial Combined static and dynamic analyses in Frama-C: An Overview at 2nd ARVI COST School on Runtime Verification, [slides]
26 Oct 2017, Tutorial Frama-C, a Collaborative Framework for C Code Verification (co-organized with Julien Signoles) at ISSRE 2017, [slides]
10 Oct 2017, Tutorial Advanced Test Coverage Criteria: Specify and Measure, Cover and Unmask (co-organized with Sébastien Bardin) at ICTSS 2017, [slides]
27 Sept 2016, Tutorial Frama-C, a Collaborative Framework for C Code Verification (co-organized with Julien Signoles) at RV 2016, [slides]
Tutorials on runtime assertion checking (co-organized with Julien Signoles) at TAP 2014 [slides], RV 2013 [slides]
Tutorials on proof of programs (co-organized with Virgile Prevosto and Julien Signoles) at TAP 2013 [slides], iFM 2013, SAC 2013 [slides]
Tutorials on structural software testing (co-organized with Nicky Williams) at ASE 2012, TAROT 2012, TAP 2012, QSIC 2012 [slides, examples]

Past News and Seminars

22 Nov 2016, Talk Formal Verification of a Memory Allocation Module of Contiki with Frama-C: a Case Study at C&ESAR 2016, [slides]
12 November 2016, Invited talk Combinations of Static and Dynamic Analyses in Frama-C: An Overview at JML 2016 workshop, [slides]
6 July 2016, Our TAP 2016 paper receives the TAP 2016 Best Paper Award, [award], [paper], [slides]
12 April 2016, Talk at Digicosme Research Days 2016, [slides]
11 February 2016, Seminar at SnT, University of Luxembourg, [slides]
24 November 2015, Invited talk at Séminaire de Saclay sur les Méthodes Formelles (SASEFOR), in Orsay, [slides]
10 September 2015, Seminar at VERIMAG, Grenoble, [slides]
01 July 2015, Seminar at Imperial College London, [slides]
30 June 2015, Invited talk at SEC2, part of COMPAS 2015, in Lille, [slides]
23 June 2015, Invited talk at USE 2015, part of FM 2015, in Oslo, [slides]
01 June 2015, Seminar at Fraunhofer FOKUS, Berlin, [slides]
8 March 2013, Formal methods and security seminar at INRIA Rennes (with Matthieu Lemerre), [slides]
March 2011, Our CSTVA 2011 tool demo receives the CSTVA 2011 Best Demo Award, [paper]

Conference and Workshop Organization

21 Nov 2024, Workshop of the working group on Software Testing MTV2 2024 of the French network on Software Engineering GDR GPL
16-17 Nov 2023, Workshop of the working group on Software Testing MTV2 2023 of the French network on Software Engineering GDR GPL
16 Mar 2023, Workshop of the working group on Software Testing MTV2 2023 of the French network on Software Engineering GDR GPL
17 Mar 2022, Workshop of the working group on Software Testing MTV2 2022 of the French network on Software Engineering GDR GPL
20 Nov 2020, Workshop of the working group on Software Testing MTV2 2020 of the French network on Software Engineering GDR GPL
March 30-April 3, 2020 in Brno, Czech Republic, Software Verification and Testing (SVT) Track of the 35th ACM/SIGAPP Symposium On Applied Computing (SAC-SVT 2020)
15-17 October 2019 in Paris, France, The 31st IFIP International Conference on Testing Software and System (IFIP-ICTSS 2019)
03 June 2019 in Paris, France, Workshop Frama-C & SPARK Day 2019
07 Dec 2018, Workshop of the working group on Software Testing MTV2 2018 (co-located with LTP 2018) of the French network on Software Engineering GDR GPL
27-28 Jun 2018, the Sound Static Analysis for Security Workshop SSAS 2018 at NIST, Washington, USA
09 Apr 2018, the Second International Workshop on Usages of Symbolic Execution USE 2018 (co-located with the 11th IEEE Conference on Software Testing, Verification and Validation ICST 2018)
07 Dec 2017, Workshop of the working group on Software Testing MTV2 2017 (co-located with MFDL 2017) of the French network on Software Engineering GDR GPL
13-14 June 2017 in Monpelier, France, French-speaking workshop AFADL 2017 co-located with GDR GPL 2017
30 May 2017 in Paris, France, Workshop Frama-C & SPARK Day 2017: Formal Analysis and Proof for Programs in C and Ada
01 Dec 2016, Workshop of the working group on Software Testing MTV2 2017 of the French network on Software Engineering GDR GPL
5 Sept 2016, Workshop CP meets Verification 2016 at CP 2016

Service

PC co-chair for iFM 2024, SAC-SVT 2021, SAC-SVT 2020, IFIP-ICTSS 2019, AFADL 2017, TAP 2015
Tutorial chair for ISSRE 2017
Steering Committee member for TAP, iFM
Previously, Steering Committee member for IFIP-ICTSS
PC member for FM 2024, FM 2024 i-Day, TAP 2024, ICST 2024, AFADL 2024, SAC-SVT 2024, AFADL 2023, iFM 2023, SAC-SVT 2023, ICST 2023, HILT 2022, iFM 2022, SAC-SVT 2022, FMICS 2022, FTfJP 2021, TAP 2021, SAC-SVT 2021, HILT 2020, IFIP-ICTSS 2020, SAC-SVT 2020, TAP 2020, AFADL 2019, iFM 2019, IFIP-ICTSS 2019, SSIoT 2019 , SEFM 2019, TAP 2019, SAC-SVT 2019, AFADL 2018, TAP 2018, HILT 2018, iFM 2018, SAC-SVT 2018, AFADL 2017, TAP 2017, SAC-SVT 2017, TAP 2016, AFADL 2016, SEC2 2016, SAC-SVT 2016, AFADL 2015, TAP 2015, SEC2 2015, TAP 2014, the Security, Dependability and Reliability in Grids and Clouds Track at 3PGCIC 2013, TAP 2013, ForMASECC 2012, TAP 2012, TAP 2011
Reviewer for several journals: Comminications of the ACM; Formal Aspects of Computing; Transactions on Programming Languages and Systems (TOPLAS); Journal of Systems and Software; Information and Software Technology; Journal of Computer Science and Technology; Science of Computer Programming; Software Testing, Verification and Reliability; Journal of Systems Architecture; Software Quality Journal.

Software and research prototypes

Test generation web service PathCrawler online
The test generation toolset LTest
Constraint solver for Sequences
Test generator for programs with Aliases
Minimal projective resolutions of simple modules over algebras of tame representation type RESOLUT
LPG Cargo Simulator

Students

Current PhD Students

Yani Ziani
Martin Hána

Previous PhD Students

Omar Chebaro. PhD Thesis "Classification de menaces d'erreurs par analyse statique, simplification syntaxique et test structurel de programmes" defended on Dec 13, 2011. Dissertation (in French)
Guillaume Petiot. PhD Thesis "Contribution à la vérification de programmes C par combinaison tests et preuves" defended on Nov 04, 2015. Dissertation (in French)
Allan Blanchard. PhD Thesis "Aide à la vérification de programmes concurrents par transformation de code et de spécifications" defended on Dec 06, 2016. Dissertation (in French)
Jean-Christophe Léchenet. PhD Thesis "Certified Algorithms for Program Slicing" defended on July 19, 2018. Dissertation
Lionel Blatter. PhD Thesis "Relational properties for specification and verification of C programs in Frama-C" defended on Sept 26, 2019. Dissertation
Virgile Robles. PhD Thesis "Specifying and Verifying High-Level Requirements on Large Programs: Application to Security of C Programs" defended on Jan 21, 2022. Dissertation
Thibault Martin. PhD Thesis "Techniques de test pour des critères de couverture avancés" defended on Nov 30, 2022. Dissertation
Dara Ly. PhD Thesis "Formalisation d'un vérificateur dynamique de propriétés mémoire pour programmes C" defended on Dec 05, 2022. Dissertation (in French)

Previous MS Students

Axel Ferréol, CentraleSupelec, Univ. Rennes, May 2024-Oct 2024
Téo Bernier, UPMC, Sorbonne Univ., Mar 2023-Sep 2023
Yani Ziani, Univ. Versailles-Saint-Quentin, Apr 2021-Oct 2021
Thibault Martin, Univ. Paris-Sud, Feb 2018-Aug 2018
Virgile Robles, ENSEIRB-MATMECA - Univ. Bordeaux, Feb 2018-Aug 2018
Quentin Molle, UTC, Sept 2017-March 2017
Quentin Bouillaguet, Univ. Paris Diderot, May-Sep 2016
Frédéric Mangano, Univ. Paris-Sud Orsay, Feb-July 2016
Filip Arvid Jakobsson, ENSEIRB, Univ. Bordeaux-1, March-Sep 2014
Thibault Lejeune, Univ. UPMC Paris-6, June-Sep 2014
Allan Blanchard, Univ. d'Orléans, Apr-Sep 2013
Guillaume Petiot, Univ. d'Orléans, Apr-Sep 2012
Céline Alec, Univ. Paris-Dauphine, May-Aug 2012
Thibaut Lefebvre, ENSIIE, Evry, Jun-Sep 2011
Nicolas Dugué, Univ. d'Orléans, May-Sep 2011
Abdelkader Kersani, Univ. Joseph Fourier Grenoble 1, May-Sep 2009
Amine Kouider, Univ. de Provence Aix-Marseille 1, Jun-Sep 2009

Postdocs

Previous Postdocs

Kostyantyn Vorobyov, Oct 2015 - Oct 2017
Michael Marcozzi, Nov 2015 - Nov 2017

Postdocs, PhD and MS thesis proposals

I regularly propose topics for postdocs, PhD and Master's theses. Motivated students are invited to contact me for more detail.

Teaching

I give/gave various lectures on Mathematics and Computer Science in several universities:

Univ. Paris-Est-Créteil-Val-de-Marne, France
Univ. Paris-Saclay, Orsay, France
CentraleSupelec, Paris-Saclay, France
Telecom SudParis, Evry, France
Univ. Pierre et Marie Curie Paris 6, Paris, France
ENSIIE, Evry, France
Univ. d'Orléans, France
Univ. de Franche-Comté, Besancon, France
RWTH-Aachen, Germany
St.Petersburg State University, Russia

Research topics All publications Education Experience