Back to the main page

Patents:

    2018:
  1. Paul Dubrulle, Stéphane Louise, Christophe Gaston, Mathieu Jan, Nikolai Kosmatov, and Arnault Lapitre.
    Outil et procédé de conception et de validation d'un système flots de données par un modèle formel. (Tool and method for design and validation of a dataflow system by a formal model).
    Patent application. In French. Submitted on August 31, 2018 to INPI (French Patent Office).


  2. 2016:
  3. Kostyantyn Vorobyov, Nikolai Kosmatov, and Julien Signoles.
    A computer-implemented method and a system for encoding a heap application memory state using shadow memory.
    Patent application. Submitted on September 27, 2016 to European Patent Office. Submitted on September 15, 2017 to US Patent Office. [pdf]

  4. Kostyantyn Vorobyov, Nikolai Kosmatov, and Julien Signoles.
    A computer-implemented method and a system for encoding a stack application memory state using shadow memory.
    Patent application. Submitted on December 7, 2016 to European Patent Office. Submitted on November 29, 2017 to US Patent Office. [pdf]


Publications:

In Computer Science:

    2019:
  1. Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov.
    Towards Full Proof Automation in Frama-C using Auto-Active Verification.
    In Proc. of the 11th NASA Formal Methods Symposium (NFM 2019),
    Houston, TX, USA, May 2019, LNCS, vol. xxx, pages xx-xx. Springer. ISBN xxx. To appear.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: xxx To appear.

  2. Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue.
    Logic against Ghosts: Comparison of two Proof Approaches for a List Module.
    Best Software Development paper award. [award]
    In Proc. of the 34th ACM/SIGAPP Symposium On Applied Computing, Software Verification and Testing Track (SAC-SVT 2019),
    Limassol, Cyprus, April 2019, pages 2186-2195. ACM. ISBN 978-1-4503-5933-7.
    [pdf] This is the authors' final version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in SAC 2019, DOI: 10.1145/3297280.3297495.

  3. Paul Dubrulle, Christophe Gaston, Nikolai Kosmatov Arnault Lapitre, and Stéphane Louise.
    A Data Flow Model with Frequency Arithmetic.
    In Proc. of the 22nd International Conference on Fundamental Approaches to Software Engineering (FASE 2019)
    part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019),
    Prague, Czech Republic, April 2019, pages 369-385. LNCS, vol. 11424. Springer. ISBN 978-3-030-16721-9.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-030-16722-6_22.

  4. Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, and Pascale Le Gall.
    MetAcsl: Specification and Verification of High-Level Properties.
    In Proc. of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019),
    part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019),
    Prague, Czech Republic, April 2019, pages 358-364. LNCS, vol. 11427. Springer. ISBN 978-3-030-17461-3.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-030-17462-0_22.


  5. 2018:
  6. Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue.
    MMFilter: A CHR-based solver for generation of executions under weak memory models.
    In Computer Languages, Systems and Structures, vol. 53, pages 121-142. Elsevier.
    [pdf] This is the authors' final version of the work. DOI: https://doi.org/10.1016/j.cl.2018.03.002.

  7. Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand.
    How Testing Helps to Diagnose Proof Failures.
    In Formal Aspects of Computing Journal, vol. 30, issue 6, pages 629-657. 2018. Springer..
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/s00165-018-0456-4.

  8. Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall.
    Cut Branches Before Looking for Bugs: Certifiably Sound Verification on Relaxed Slices.
    In Formal Aspects of Computing Journal, vol. 30, issue 1, pages 107-131. 2018. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/s00165-017-0439-x

  9. Dara Ly, Nikolai Kosmatov, Julien Signoles, Frédéric Loulergue.
    Soundness of a Dataflow Analysis for Memory Monitoring.
    In Proc. of the 5th International Workshop on Languages and Tools for Ensuring Cyber-Resilience in Critical Software-Intensive Systems (HILT 2018),
    part of the ACM SIGPLAN Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH 2018)

    Boston, USA, November 2018, pages xx-xx. ACM. ISBN xxx. To appear.
    [pdf] This is the authors' final version of the work.

  10. Sébastien Bardin, Nikolai Kosmatov, Bruno Marre, David Mentré, Nicky Williams.
    Test Case Generation with Pathcrawler/LTest: How to Automate an Industrial Testing Process.
    In Proc. of the 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2018),
    Limassol, Cyprus, November 2018, LNCS, vol. 11247, pages 104-120. Springer. ISBN 978-3-030-03426-9.
    [pdf] [slides] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-030-03427-6_12.

  11. Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue.
    A Lesson on Verification of IoT Software with Frama-C.
    In Proc. of the 12th International Conference on High Performance Computing & Simulation (HPCS 2018),
    Orléans, France, July 2018, pages 21-30. IEEE. ISBN 978-1-5386-7878-7.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/HPCS.2018.00018.

  12. Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles.
    Detection of Security Vulnerabilities in C Code using Runtime Verification: an Experience Report.
    In Proc. of the 12th International Conference on Tests & Proofs (TAP 2018),
    Toulouse, France, June 2018, pages 139-156. LNCS, vol. 10889. Springer. ISBN 978-3-319-92993-4.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-92994-1_8.

  13. Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto, Guillaume Petiot.
    Static and Dynamic Verification of Relational Properties on Self-Composed C Code.
    In Proc. of the 12th International Conference on Tests & Proofs (TAP 2018),
    Toulouse, France, June 2018, pages 44-62. LNCS, vol. 10889. Springer. ISBN 978-3-319-92993-4.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-92994-1_3.

  14. Frédéric Loulergue, Allan Blanchard, Nikolai Kosmatov.
    Ghosts for Lists: from Axiomatic to Executable Specifications.
    In Proc. of the 12th International Conference on Tests & Proofs (TAP 2018),
    Toulouse, France, June 2018, pages 177-184. LNCS, vol. 10889. Springer. ISBN 978-3-319-92993-4.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-92994-1_11.

  15. Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov.
    Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C.
    In Proc. of the 10th NASA Formal Methods Symposium (NFM 2018),
    Newport News, VA, USA, April 2018, LNCS, vol. 10811, pages 37-53. Springer. ISBN 978-3-319-77934-8.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: http://dx.doi.org/10.1007/978-3-319-77935-5_3.

  16. Michaël Marcozzi, Sébastien Bardin, Nikolai Kosmatov, Mike Papadakis, Virgile Prevosto and Loïc Correnson.
    Time to Clean your Test Objectives.
    In Proc. of the 40th International Conference on Software Engineering (ICSE 2018),
    Gothenburg, Sweden, June 2018, pages 456-467. ACM. ISBN 978-1-4503-5638-1.
    [pdf] This is the authors' final version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ICSE 2018, http://doi.acm.org/10.1145/3180155.3180191.

  17. Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall.
    Fast Computation of Arbitrary Control Dependencies.
    In Proc. of the 21st International Conference on Fundamental Approaches to Software Engineering (FASE 2018)
    part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2018),
    Thessaloniki, Greece, April 2018, pages 207-224. LNCS, vol. 10802. Springer. ISBN 978-3-319-89362-4.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: https://doi.org/10.1007/978-3-319-89363-1_12.

  18. Alexandre Peyrard, Nikolai Kosmatov, Simon Duquennoy, Shahid Raza.
    Towards Formal Verification of Contiki OS: Analysis of the AES-CCM* Modules with Frama-C.
    In Proc. of the 2nd International Workshop on Recent advances in secure management of data and resources in the IoT (RED-IoT 2018),
    part of the International Conference on Embedded Wireless Systems and Networks (EWSN 2018),
    Madrid, Spain, February 2018, pages 264-269. ACM.
    [pdf] This is the authors' final version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in RED-IOT 2018, http://dl.acm.org/citation.cfm?id=3234910.

  19. Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall.
    Why3 a dit : gardez le contrôle en toute situation.
    In 29mes Journées Francophones des Langages Applicatifs (JFLA 2018)
    Banyuls-sur-Mer, France, January 2018, 7 pages. (In French).
    [pdf]


  20. 2017:
  21. Julien Signoles, Nikolai Kosmatov and Kostyantyn Vorobyov.
    E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs (tool paper).
    In Proc. of the 1st International Workshop on Competitions, Usability,
    Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES 2017),
    part of the 17th International Conference on Runtime Verification (RV 2017),

    Seattle, USA, September 2017, Kalpa Publications in Computing, vol. 3, pages 164-173, ISSN: 2515-1762.
    [pdf] This is the authors' final version of the work.

  22. Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles and Arvid Jakobsson.
    Runtime Detection of Temporal Memory Errors.
    In Proc. of the 17th International Conference on Runtime Verification (RV 2017),
    Seattle, USA, September 2017, LNCS, vol. 10548, pages 294-311. Springer. ISBN 978-3-319-67530-5.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-67531-2_18.

  23. Kostyantyn Vorobyov, Julien Signoles, and Nikolai Kosmatov.
    Shadow State Encoding for Efficient Monitoring of Block-level Properties.
    In Proc. of the 2017 ACM SIGPLAN International Symposium on Memory Management (ISMM 2017),
    Barcelona, Spain, June 2017, pages 47-58, ACM. ISBN 978-1-4503-5044-0.
    [pdf] This is the authors' final version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ISMM 2017, http://doi.acm.org/10.1145/3092255.3092269

  24. Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov.
    From Concurrent Programs to Sequential Simulating Programs: Correctness of a Transformation.
    In Proc. of the 5th International Workshop on Verification and Program Transformation (VPT 2017), ETAPS 2017 Workshops,
    Uppsala, Sweden, April 2017, EPTCS, vol. 253, pages 109-123.
    [pdf] This is the authors' final version of the work. DOI: 10.4204/EPTCS.253.9.

  25. Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall and Virgile Prevosto.
    RPP: Automatic Proof of Relational Properties by Self-Composition.
    In Proc. of the 23th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017),
    part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2017),
    Uppsala, Sweden, April 2017, LNCS, vol. 10205, pages 391-397. Springer. ISBN 978-3-662-54576-8.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-662-54577-5_22.

  26. Michaël Marcozzi, Mickaël Delahaye, Sébastien Bardin, Nikolai Kosmatov and Virgile Prevosto.
    Generic and Effective Specification of Structural Test Objectives.
    In Proc. of the 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017),
    Tokyo, Japan, March 2017, pages 436-441. IEEE. ISBN 978-1-5090-6031-3.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/ICST.2017.48

  27. Michaël Marcozzi, Sébastien Bardin, Mickaël Delahaye, Nikolai Kosmatov and Virgile Prevosto.
    Taming Coverage Criteria Heterogeneity with LTest.
    In Proc. of the 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017),
    Tokyo, Japan, March 2017, pages 500-507. IEEE. ISBN 978-1-5090-6031-3.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/ICST.2017.57


  28. 2016:
  29. Arvid Jakobsson, Nikolai Kosmatov and Julien Signoles.
    Fast as a shadow, expressive as a tree: Optimized memory monitoring for C.
    In Science of Computer Programming,
    2016, vol. 132, part 2, pages 226-246,. ISSN 0167-6423.
    [pdf] This is the authors' final version of the work. The final publication was published in Sci. Comput. Program., DOI: 10.1016/j.scico.2016.09.003

  30. Nikolai Kosmatov, Claude Marché, Yannick Moy, Julien Signoles.
    Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014.
    In Proc. of the 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2016),
    Corfu, Greece, October 2016, LNCS, vol. 9952, pages 461-478. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-47166-2_32.

  31. Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue.
    Conc2Seq : A Frama-C Plugin for Verification of Parallel Compositions of C Programs.
    In Proc. of the 16th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2016),
    Raleigh, NC, USA, October 2016, pages 67-72. IEEE. ISBN 978-1-5090-3848-0.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/SCAM.2016.18.

  32. Nikolai Kosmatov, Julien Signoles.
    Frama-C, a Collaborative Framework for C Code Verification. Tutorial Synopsis.
    In Proc. of the 7th International Conference on Runtime Verification (RV 2016),
    Madrid, Spain, September 2016, LNCS, vol. 10012, pages 92-115. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-46982-9_7.

  33. Frédéric Mangano, Simon Duquennoy and Nikolai Kosmatov.
    A Memory Allocation Module of Contiki Formally Verified with Frama-C. A Case Study.
    In Proc. of the 11th International Conference on Risks and Security of Internet and Systems (CRiSIS 2016),
    Roscoff, France, September 2016, LNCS, vol. 10158, pages 114-120. Springer. ISBN 978-3-319-54875-3.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-54876-0_9.

  34. Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue.
    A CHR-Based Solver for Weak Memory Behaviors.
    In Proc. of the 7th International Workshop on Constraint Solvers in Testing, Verification, and Analysis (CSTVA 2016), ISSTA 2016 Workshops,
    Saarbruecken, Germany, July 2016, pages 15-22. CEUR Workshop Proceedings, vol. 1639.
    [pdf]

  35. Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand.
    Your Proof Fails? Testing Helps to Find the Reason.
    Best paper award. [award]
    In Proc. of the 10th International Conference on Tests & Proofs (TAP 2016),
    Vienna, Austria, July 2016, pages 130-150. LNCS, vol. 9762. Springer. ISBN 978-3-319-41134-7.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-41135-4_8.

  36. Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall.
    Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices.
    In Proc. of the 19th International Conference on Fundamental Approaches to Software Engineering (FASE 2016)
    part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2016),
    Eindhoven, The Netherlands, April 2016, pages 179-196. LNCS, vol. 9633. Springer. ISBN 978-3-662-49664-0.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-662-49665-7_11.

  37. Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall.
    Coq a dit : fromage tranché ne peut cacher ses trous.
    In 27mes Journées Francophones des Langages Applicatifs (JFLA 2016)
    Saint-Malo, France, January 2016, 3 pages. (In French).
    [pdf]


  38. 2015:
  39. Balázs Kiss, Nikolai Kosmatov, Dillon Pariente and Armand Puccetti.
    Combining Static and Dynamic Analyses for Vulnerability Detection: Illustration on Heartbleed.
    In Proc. of the 11th Haifa Verification Conference (HVC 2015),
    Haifa, Israel, November 2015, pages 39-50. LNCS, vol. 9434. Springer. ISBN 978-3-319-26286-4.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-26287-1

  40. Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue.
    A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C.
    In Proc. of the 20th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2015),
    Oslo, Norway, June 2015, pages 15-30. LNCS, vol. 9128. Springer. ISBN 978-3-319-19457-8.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-19458-5_2

  41. Sébastien Bardin, Mickaël Delahaye, Robin David, Nikolai Kosmatov, Mike Papadakis, Yves Le Traon and Jean-Yves Marion.
    Sound and Quasi-Complete Detection of Infeasible Test Requirements.
    In Proc. of the 8th IEEE International Conference on Software Testing, Verification and Validation (ICST 2015),
    Graz, Austria, April 2015, pages 1-10. IEEE. ISBN 978-1-4799-7125-1.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/ICST.2015.7102607

  42. Arvid Jakobsson, Nikolai Kosmatov and Julien Signoles.
    Fast as a Shadow, Expressive as a Tree: Hybrid Memory Monitoring for C.
    In Proc. of the 30th ACM/SIGAPP Symposium On Applied Computing, Software Verification and Testing Track (SAC-SVT 2015),
    Salamanca, Spain, April 2015, pages 1765-1772. ACM. ISBN 978-1-4503-3196-8.
    [pdf] This is the authors' final version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in SAC 2015, DOI: 10.1145/2695664.2695815

  43. Arvid Jakobsson, Nikolai Kosmatov and Julien Signoles.
    Rester statique pour devenir plus rapide, plus précis et plus mince.
    In 26mes Journées Francophones des Langages Applicatifs (JFLA 2015)
    Val d'Ajol, France, January 2015, 15 pages. (In French)
    [pdf]

  44. Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski.
    Frama-C: A Program Analysis Perspective.
    In Formal Aspects of Computing Journal, vol. 27, issue 3, pages 573-609. 2015. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/s00165-014-0326-7


  45. 2014:
  46. Guillaume Petiot, Bernard Botella, Jacques Julliand, Nikolai Kosmatov, Julien Signoles.
    Instrumentation of Annotated C Programs for Test Generation.
    In Proc. of the 14th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2014),
    Victoria, Canada, September 2014, pages 105-114. IEEE. ISBN 978-0-7695-5304-7.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/SCAM.2014.19

  47. Sébastien Bardin, Omar Chebaro, Mickaël Delahaye, Nikolai Kosmatov.
    An All-in-one Toolkit for Automated White-Box Testing.
    In Proc. of the 8th International Conference on Tests & Proofs (TAP 2014),
    York, UK, July 2014, pages 53-60. LNCS, vol. 8570. Springer. ISBN 978-3-319-09098-6.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-09099-3_4

  48. Nikolai Kosmatov, Matthieu Lemerre, Céline Alec.
    A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing.
    In Proc. of the 8th International Conference on Tests & Proofs (TAP 2014),
    York, UK, July 2014, pages 158-164. LNCS, vol. 8570. Springer. ISBN 978-3-319-09098-6.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-09099-3_12

  49. Nikolai Kosmatov, Julien Signoles.
    Runtime Assertion Checking and its Combinations with Static and Dynamic Analyses. Tutorial Synopsis.
    In Proc. of the 8th International Conference on Tests & Proofs (TAP 2014),
    York, UK, July 2014, pages 165-168. LNCS, vol. 8570. Springer. ISBN 978-3-319-09098-6.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-09099-3_13

  50. Guillaume Petiot, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand.
    How Test Generation Helps Software Specification and Deductive Verification in Frama-C.
    In Proc. of the 8th International Conference on Tests & Proofs (TAP 2014),
    York, UK, July 2014, pages 204-211. LNCS, vol. 8570. Springer. ISBN 978-3-319-09098-6.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-319-09099-3_16

  51. Sébastien Bardin, Nikolai Kosmatov, François Cheynier.
    Efficient Leverage of Symbolic ATG Tools to Advanced Coverage Criteria.
    In Proc. of the 7th IEEE International Conference on Software Testing, Verification and Validation (ICST 2014),
    Cleveland, Ohio, USA, March-April 2014, pages 173-182. IEEE. ISBN 978-0-7695-5185-2.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/ICST.2014.30

  52. Omar Chebaro, Pascal Cuoq, Nikolai Kosmatov, Bruno Marre, Anne Pacalet, Nicky Williams, Boris Yakobowski.
    Behind the Scenes in SANTE: A Combination of Static and Dynamic Analyses.
    In Automated Software Engineering Journal, vol. 21(1), pages 107-143. 2014. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/s10515-013-0127-x


  53. 2013:
  54. Nikolai Kosmatov, Guillaume Petiot, Julien Signoles.
    An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs.
    In Proc. of the 4th International Conference on Runtime Verification (RV 2013),
    Rennes, France, September 2013, LNCS, vol. 8174, pages 167-182. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-642-40787-1_10

  55. Mickaël Delahaye, Nikolai Kosmatov.
    A Late Treatment of C Precondition in Dynamic Symbolic Execution Testing Tools.
    In Proc. of the 4th International Conference on Runtime Verification (RV 2013),
    Rennes, France, September 2013, LNCS, vol. 8174, pages 328-333. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-642-40787-1_20

  56. Nikolai Kosmatov, Julien Signoles.
    A Lesson on Runtime Assertion Checking with Frama-C.
    In Proc. of the 4th International Conference on Runtime Verification (RV 2013),
    Rennes, France, September 2013, LNCS, vol. 8174, pages 386-399. Springer.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-642-40787-1_29

  57. Nikolai Kosmatov, Virgile Prevosto, Julien Signoles.
    A Lesson on Proof of Programs with Frama-C. Invited Tutorial Paper.
    In Proc. of the 7th International Conference on Tests and Proofs (TAP 2013),
    Budapest, Hungary, June 2013, LNCS, vol. 7942, pages 168-177. Springer.
    [pdf] This is the authors' final version of the work. The final publication will be available at http://link.springer.com. DOI: 10.1007/978-3-642-38916-0_10

  58. Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger.
    Strucutural Unit Testing as a Service with PathCrawler-online.com.
    In Proc. of the 7th IEEE International Symposium on Service Oriented System Engineering (SOSE 2013),
    San Francisco Bay, USA, March 2013, pages 435-440. ISBN 978-0-7695-4944-6.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/SOSE.2013.78.

  59. Mickaël Delahaye, Nikolai Kosmatov.
    A Late Treatment of C Precondition in Dynamic Symbolic Execution.
    In Proc. of the 5th International Workshop on Constraints in Software Testing, Verification, and Analysis (CSTVA 2013), ICST Workshops,
    Luxembourg, March 2013, pages 230-231. IEEE. ISBN 978-1-4799-1324-4.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/ICSTW.2013.34.

  60. Mickaël Delahaye, Nikolai Kosmatov, Julien Signoles.
    Common Specification Language for Static and Dynamic Analysis of C Programs.
    In Proc. of the 28th Annual ACM Symposium On Applied Computing, Software Verification and Testing Track (SAC-SVT 2013),
    Coimbra, Portugal, March 2013, pages 1230--1235, ACM. ISBN 978-1-4503-1656-9.
    [pdf] This is the authors' final version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in SAC 2013, http://dx.doi.org/10.1145/2480362.2480593

  61. Nikolai Kosmatov.
    Concolic Test Generation and the Cloud: Deployment and Verification Perspectives.
    Chapter 11 in Software Testing in the Cloud: Perspectives on an Emerging Discipline
    pages 231-251. IGI Global, 2013. ISBN 978-1-46662-536-5.
    [pdf] This is the author's final version of the work.


  62. 2012:
  63. Matthieu Lemerre, Nikolai Kosmatov, Céline Alec.
    Verified secure kernels and hypervisors for the cloud.
    In Proc. of Computer and Electronics Security Applications Rendez-vous (C&ESAR 2012),
    Rennes, France, November 2012, pages 89--104.
    [pdf] This paper is not a formal archieval publication.

  64. Omar Chebaro, Mickaël Delahaye, Nikolai Kosmatov.
    Testing Inexecutable Conditions on Input Pointers in C Programs with SANTE.
    In Proc. of the 24th International Conference on Software & Systems Engineering and their Applications (ICSSEA 2012),
    Paris, France, October 2012.
    [pdf] This is the authors' final version of the work.

  65. Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski.
    Frama-C: A Program Analysis Perspective.
    In Proc. of the 10th International Conference on Software Engineering and Formal Methods (SEFM 2012),
    Thessaloniki, Greece, October 2012, LNCS, vol. 7504, pages 233-247. Springer. ISBN 978-3-642-33825-0.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-642-33826-7_16

  66. Nicky Williams, Nikolai Kosmatov.
    Structural Testing with PathCrawler. Tutorial Synopsis.
    In Proc. of the 12th International Conference on Quality Software (QSIC 2012),
    Xi'an, China, August 2012, pages 289-292. IEEE. ISBN 978-0-7695-4833-3.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/QSIC.2012.24

  67. Frédéric Loulergue, Frédéric Gava, Nikolai Kosmatov, Matthieu Lemerre.
    Towards Verified Cloud Computing Environments.
    In Proc. of the 2012 International Conference on High Performance Computing and Simulation (HPCS 2012),
    Madrid, Spain, July 2012, pages 91-97. IEEE. ISBN 978-1-4673-2359-8.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/HPCSim.2012.6266896

  68. Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger, Omar Chebaro.
    A lesson on structural testing with pathcrawler-online.com.
    In Proc. of the 6th International Conference on Tests and Proofs (TAP 2012),
    Prague, Czech Republic, May-June 2012, LNCS, vol. 7305, pages 169-175. Springer. ISBN 978-3-642-30472-9.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-642-30473-6_15

  69. Nikolai Kosmatov, Nicky Williams.
    Tutorial on Automated Structural Testing with PathCrawler -- Extended Abstract.
    In Proc. of the 6th International Conference on Tests and Proofs (TAP 2012),
    Prague, Czech Republic, May-June 2012, LNCS, vol. 7305, pages 176. Springer. ISBN 978-3-642-30472-9.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-642-30473-6_16

  70. Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand.
    Program Slicing Enhances a Verification Technique Combining Static and Dynamic Analysis.
    In Proc. of the 27th Annual ACM Symposium On Applied Computing, Software Verification and Testing Track (SAC-SVT 2012),
    Riva del Garda (Trento), Italy, March 2012, pages 1284--1291, ACM. ISBN 978-1-4503-0857-1.
    [pdf] This is the authors' final version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in SAC 2012, http://dx.doi.org/10.1145/2245276.2231980


  71. 2011:
  72. Nikolai Kosmatov, Bernard Botella, Muriel Roger, Nicky Williams.
    Online Test Generation with PathCrawler. Tool demo.
    Best demo award.
    In Proc. of the 3rd International Workshop on Constraints in Software Testing, Verification, and Analysis (CSTVA 2011), ICST Workshops,
    Berlin, Germany, March 2011, pages 316-317. IEEE. ISBN 978-1-4577-0019-4.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/ICSTW.2011.85.

  73. Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand.
    The SANTE Tool: Value Analysis, Program Slicing and Test Generation for C Program Debugging.
    In Proc. of the 5th International Conference on Tests and Proofs (TAP 2011),
    Zurich, Switzerland, June-July 2011, LNCS, vol. 6706, pages 78-83. Springer. ISBN 978-3-642-21767-8.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-642-21768-5_7


  74. 2010:
  75. Nikolai Kosmatov.
    Génération de tests "tous-les-chemins" : quelle complexité pour quelles contraintes?.
    In Actes des Sixièmes Journées Francophones de Programmation par Contraintes (JFPC 2010),
    Caen, France, Juin 2010, pages 187-196.
    [pdf]

  76. Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand.
    Combining Static Analysis and Test Generation for C Program Debugging.
    In Proc. of the 4th International Conference on Tests and Proofs (TAP 2010),
    Malaga, Spain, July 2010, LNCS, vol. 6143, pages 94-100. Springer. ISBN 978-3-642-13976-5.
    [pdf] This is the authors' final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/978-3-642-13977-2_9

  77. Nikolai Kosmatov.
    Constraint-Based Techniques for Software Testing.
    Chapter 11 in Artificial Intelligence Applications for Improved Software Engineering Development: New Prospects
    Advances in Intelligent Information Technologies Book Series

    pages 218-232. IGI Global, 2010. ISBN 978-1-60566-758-4.
    [pdf] This is the author's final version of the work.


  78. 2009:
  79. Nikolai Kosmatov.
    On Complexity of All-Paths Test Generation. From Practice to Theory.
    In Proc. of the Testing: Academic and Industrial Conference - Practice and Research Techniques (TAIC PART 2009),
    Windsor, United Kingdom, September 2009, pages 144-153. IEEE Computer Society Press. ISBN 978-0-7695-3820-4.
    [pdf] This is the author's final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/TAICPART.2009.26

  80. Bernard Botella, Mickaël Delahaye, Stéphane Hong-Tuan-Ha, Nikolai Kosmatov, Patricia Mouy, Muriel Roger, Nicky Williams.
    Automating Structural Testing of C Programs: Experience with PathCrawler
    In Proc. of the Fourth International Workshop on the Automation of Software Test (AST 2009),
    part of the 31st International Conference on Software Engineering (ICSE 2009),

    Vancouver, Canada, May 2009, pages 70-78. IEEE Computer Society Press.
    [pdf] This is the authors' final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/IWAST.2009.5069043


  81. 2008:
  82. Nikolai Kosmatov.
    All-paths test generation for programs with internal aliases.
    In Proc. of the 19th IEEE Int. Symp. on Software Reliability Engineering (ISSRE 2008),
    Redmond, Seattle, USA, November 2008, pages 147-156. IEEE Computer Society Press. ISBN 978-1-4244-3417-6.
    [pdf] This is the author's final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/ISSRE.2008.25


  83. 2006:
  84. Nikolai Kosmatov.
    Constraint Solving for Sequences in Software Validation and Verification.
    In M. Umeda, A. Wolf et al., editors,
    Revised Selected Papers of the 16th International Conference on Applications of Declarative Programming and Knowledge Management (INAP 2005),
    Fukuoka, Japan, October 2005, LNCS, vol. 4369, pages 25-37. Springer, 2006. ISBN 978-3-540-69233-1. DOI: 10.1007/11963578_3.

  85. Nikolai Kosmatov.
    A Constraint Solver for Sequences and its Applications.
    In Proc. of the 21st Annual ACM Symposium on Applied Computing, Constraint Solving and Programming Track (SAC-SCP 2006),
    Dijon, France, April 2006, pages 404-408. ACM Press. ISBN: 1-59593-108-2.
    [pdf] © ACM, 2006.
    This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in SAC 2006, http://doi.acm.org/10.1145/1141277.1141369

  86. Yohan Boichut, Nikolai Kosmatov, Laurent Vigneron.
    Validation of Prouvé protocols using the automatic tool TA4SP.
    In Proc. of the Third Taiwanese-French Conference on Information Technology (TFIT 2006),
    Nancy, France, March 2006, pages 467-480.
    [pdf]


  87. 2005:
  88. Jean-François Couchot, Alain Giorgetti, Nikolai Kosmatov.
    A uniform deductive approach for parameterized protocol safety.
    In Proc. of the 20th IEEE/ACM International Conference on Automated Software Engineering (ASE 2005),
    Long Beach, California, USA, November 2005, pages 364-367. IEEE Computer Society Press. ISBN: 1-59593-993-4.
    [pdf] © ACM, 2005.
    This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ASE 2005, http://doi.acm.org/10.1145/1101908.1101971

  89. Nikolai Kosmatov.
    A Constraint Solver for Sequences.
    In Proc. of the 1st Int. Workshop on Constraint Programming Beyond Finite Integer Domains (BeyondFD 2005),
    part of the 11th International Conference on Principles and Practice of Constraint Programming (CP 2005),

    Sitges (Barcelona), Spain, October 2005, pages 49-54.
    [pdf]


  90. 2004:
  91. Nikolai Kosmatov, Bruno Legeard, Fabien Peureux, Mark Utting.
    Boundary coverage criteria for test generation from formal models.
    In Proc. of the 15th IEEE Int. Symp. on Software Reliability Engineering (ISSRE 2004),
    Saint-Malo, France, November 2004, pages 139-150. IEEE Computer Society Press. ISBN 0-7695-2215-7.
    [pdf] This is the author's final version of the work. The final publication is available at http://ieeexplore.ieee.org/. DOI: 10.1109/ISSRE.2004.12

  92. In Mathematics:

    2007:
  93. Alexander Generalov, Nikolai Kosmatov.
    Projective resolutions and Yoneda algebras for algebras of dihedral type.
    Algebras and Repr. Theory. 10 (2007), no. 3, 241-256. Springer.
    [pdf] This is the author's final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/s10468-006-9012-7


  94. 2004:
  95. Alexander Generalov, Nikolai Kosmatov.
    Projective resolutions and Yoneda algebras for algebras of dihedral type: the family D(3Q).
    Fund. Appl. Math. 10 (2004), no. 4, 65-89.
    [pdf] This is the author's final version of the work.


  96. 2003:
  97. Alexander Generalov, Nikolai Kosmatov.
    Computation of the Yoneda algebras for algebras of dihedral type.
    J. Math. Sci. 130 (2005), no. 3, 4699-4711. Springer.
    Russian version in
    Zap. Nauchn. Sem. S.-Peterburg. Otdel. Mat. Inst. Steklov. (POMI) 305 (2003), 101-120.
    [pdf] This is the author's final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1007/s10958-005-0364-z


  98. 2002:
  99. Nikolai Kosmatov.
    On the homological dimensions of pullbacks. II.
    Théorie des nombres, Années 1998/2001, 4 pp.,
    Publ. Math. UFR Sci. Tech. Besançon, Univ. Franche-Comté, Besançon, 2002.


  100. 2000:
  101. Nikolai Kosmatov.
    Bounds on Homological Dimensions of Pullbacks. II.
    J. Math. Sci. 116 (2003), no. 1, 3014-3015. Springer.
    Russian version in
    Zap. Nauchn. Sem. S.-Peterburg. Otdel. Mat. Inst. Steklov. (POMI) 272 (2000), 234-237.
    [pdf] This is the author's final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1023/A:1023551328399


  102. 1999:
  103. Nikolai Kosmatov.
    Bounds for the Homological Dimensions of Pullbacks.
    J. Math. Sci. 112 (2002), no. 4, 4367-4370. Springer.
    Russian version in
    Zap. Nauchn. Sem. S.-Peterburg. Otdel. Mat. Inst. Steklov.(POMI) 265 (1999), 222-228.
    [pdf] This is the author's final version of the work. The final publication is available at http://link.springer.com. DOI: 10.1023/A:1020351104689

  104. Nikolai Kosmatov.
    An estimate for the global dimension of pullback rings. (In Russian)
    Fund. Appl. Math. 5 (1999), no. 4, 1251-1253.
    [pdf] This is the author's final version of the work.

  105. Nikolai Kosmatov.
    On the global and weak dimensions of pullbacks of non-commutative rings.
    Théorie des nombres, Années 1996/97-1997/98, 7 pp.,
    Publ. Math. UFR Sci. Tech. Besançon, Univ. Franche-Comté, Besançon, 1999.

Back to the main page