Research

Before I wrote here, I spent several years on research in software verification and testing, mostly asking how testing and formal proof can help each other. This is that earlier work, kept for the record.

Selected

Everything, by date

  1. Paper

    Static and Dynamic Verification of Relational Properties on Self-Composed C Code

    Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto, Guillaume Petiot

    PDF (author preview) for Static and Dynamic Verification of Relational Properties on Self-Composed C CodeSpringer for Static and Dynamic Verification of Relational Properties on Self-Composed C Code

  2. Paper

    How Testing Helps to Diagnose Proof Failures

    Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand

    PDF (author preview) for How Testing Helps to Diagnose Proof FailuresACM for How Testing Helps to Diagnose Proof FailuresBenchmarking suite for How Testing Helps to Diagnose Proof Failures

  3. Paper

    FISSC - A Fault Injection and Simulation Secure Collection

    Louis Dureuil, Guillaume Petiot, Marie-Laure Potet, Thanh-Ha Le, Aude Crohen, Philippe de Choudens

    PDF (author preview) for FISSC - A Fault Injection and Simulation Secure CollectionSpringer for FISSC - A Fault Injection and Simulation Secure Collection

  4. Paper

    Your Proof Fails? Testing Helps to Find the Reason

    Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand

    Best Paper Award for Your Proof Fails? Testing Helps to Find the ReasonPDF (author preview) for Your Proof Fails? Testing Helps to Find the ReasonSpringer for Your Proof Fails? Testing Helps to Find the Reason

  5. Paper

    Contribution to C Program Verification by Combining Tests and Proofs

    Guillaume Petiot

    PDF (last revision) for Contribution to C Program Verification by Combining Tests and ProofsSubmitted for Contribution to C Program Verification by Combining Tests and Proofs

  6. Paper

    Sequential Generation of Structured Arrays and Its Deductive Verification

    Richard Genestier, Alain Giorgetti, Guillaume Petiot

    PDF (author preview) for Sequential Generation of Structured Arrays and Its Deductive VerificationSpringer for Sequential Generation of Structured Arrays and Its Deductive Verification

  7. Paper

    Instrumentation of Annotated C Programs for Test Generation

    Guillaume Petiot, Bernard Botella, Jacques Julliand, Nikolai Kosmatov, Julien Signoles

    PDF (author preview) for Instrumentation of Annotated C Programs for Test GenerationIEEE for Instrumentation of Annotated C Programs for Test Generation

  8. Talk

    Instrumentation of Annotated C Programs for Test Generation

    14th IEEE International Working Conference on Source Code Analysis and Manipulation, Victoria, British Columbia, Canada

    Conference for Instrumentation of Annotated C Programs for Test Generation

  9. Paper

    How Test Generation Helps Software Specification and Deductive Verification in Frama-C

    Guillaume Petiot, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand

    PDF (author preview) for How Test Generation Helps Software Specification and Deductive Verification in Frama-CSpringer for How Test Generation Helps Software Specification and Deductive Verification in Frama-C

  10. Talk

    How Test Generation Helps Software Specification and Deductive Verification

    8th International Conference on Tests & Proofs, York, UK

    Conference for How Test Generation Helps Software Specification and Deductive Verification

  11. Paper

    An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs

    Nikolai Kosmatov, Guillaume Petiot, Julien Signoles

    PDF (author preview) for An Optimized Memory Monitoring for Runtime Assertion Checking of C ProgramsSpringer for An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs

  12. Paper

    Functional Parallel Programming with Revised Bulk Synchronous Parallel ML

    Wadoud Bousdira, Frederic Gava, Louis Gesbert, Frederic Loulergue, Guillaume Petiot

    PDF (author preview) for Functional Parallel Programming with Revised Bulk Synchronous Parallel MLIEEE for Functional Parallel Programming with Revised Bulk Synchronous Parallel ML