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.
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]
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]
26 June 2017, Invited talk Advanced Test Coverage Criteria: Specification and Support in Automatic Testing Tools at the 13th Summer School on Software Testing, Verification & Validation TAROT 2017, [slides]
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]
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
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.
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
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