Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

12 résultats
Page :
triés par

A Lesson on Verification of IoT Software with Frama-C

 Allan Blanchard , Nikolai Kosmatov , Frédéric Loulergue
2018 International Conference on High Performance Computing & Simulation (HPCS), Jul 2018, Orleans, France. pp.21-30, ⟨10.1109/HPCS.2018.00018⟩
Communication dans un congrès hal-02317078v1
Image document

A CHR-Based Solver for Weak Memory Behaviors

 Allan Blanchard , Nikolai Kosmatov , Frédéric Loulergue
7th Workshop on Constraint Solvers in Testing, Verification, and Analysis (CSTVA), Jul 2016, Saarbrücken, Germany
Communication dans un congrès hal-01318432v1
Image document

Ghosts for Lists: from Axiomatic to Executable Specifications

 Frédéric Loulergue , Allan Blanchard , Nikolai Kosmatov
TAP 2018 - 12th International Conference on Tests and Proofs, Jun 2018, Toulouse, France. ⟨10.1007/978-3-319-92994-1_11⟩
Communication dans un congrès hal-01811922v1

Towards Full Proof Automation in Frama-C Using Auto-active Verification

 Allan Blanchard , Frédéric Loulergue , Nikolai Kosmatov
NFM 2019 - 11th Annual NASA Formal Methods Symposium, May 2019, Houston, TX, United States. pp.88-105, ⟨10.1007/978-3-030-20652-9_6⟩
Communication dans un congrès hal-02317055v1

Assisted Concurrent Program Verification by Code and Specification Transformation

 Allan Blanchard
Génie logiciel [cs.SE]. Université d'Orléans (UO), 2016. Français. ⟨NNT : ⟩
Thèse tel-03624110v1
Image document

Logic against Ghosts: Comparison of Two Proof Approaches for a List Module

 Allan Blanchard , Nikolai Kosmatov , Frédéric Loulergue
SAC 2019 - The 34th ACM/SIGAPP Symposium On Applied Computing, Apr 2019, Limassol, Cyprus. ⟨10.1145/3297280.3297495⟩
Communication dans un congrès hal-02100515v1
Image document

Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C

 Allan Blanchard , Nikolai Kosmatov , Frédéric Loulergue
Tenth NASA Formal Methods Symposium - NFM 2018, Apr 2018, Newport News, United States. ⟨10.1007/978-3-319-77935-5_3⟩
Communication dans un congrès hal-01720401v1
Image document

A case study on formal verification of the anaxagoros hypervisor paging system with frama-C

 Allan Blanchard , N. Kosmatov , M. Lemerre , Frédéric Loulergue
FMICS 2015 - Formal Methods for Industrial Critical Systems, Jun 2015, Oslo, Norway. pp.15-30, ⟨10.1007/978-3-319-19458-5_2⟩
Communication dans un congrès cea-01834977v1

Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs

 Allan Blanchard , Nikolai Kosmatov , Matthieu Lemerre , Frédéric Loulergue
2016 IEEE 16th International Working Conference on Source Code Analysis and Manipulation (SCAM), 2016, Raleigh, NC, United States. pp.6, ⟨10.1109/SCAM.2016.18⟩
Communication dans un congrès hal-01423641v1
Image document

Des listes et leurs fantômes : vérification d'un module critique de Contiki avec FRAMA-C

 Allan Blanchard , Nikolai Kosmatov , Frédéric Loulergue
17èmes Journées AFADL : Approches Formelles Dans L'assistance Au Développement De Logiciels, Jun 2018, Toulouse, France
Communication dans un congrès hal-01811932v1
Image document

MMFilter: A CHR-Based Solver for Generation of Executions under Weak Memory Models

 Allan Blanchard , Nikolai Kosmatov , Frédéric Loulergue
Computer Languages, Systems and Structures, 2018, 53, pp.121-142. ⟨10.1016/j.cl.2018.03.002⟩
Article dans une revue hal-01777123v1

From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation

 Allan Blanchard , Frédéric Loulergue , Nikolai Kosmatov
Fifth International Workshop on Verification and Program Transformation (VPT 2017), Apr 2017, Uppsala, Sweden. ⟨10.4204/EPTCS.253.9⟩
Communication dans un congrès hal-01495454v1
Page :