Une sémantique à pas de géant pour la catégorisation des contre-exemples

Autor: BECKER, Benedikt, BELO LOURENÇO, Cláudio, MARCHÉ, Claude

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od______9631::f657d8540cce80e497c4df6e1d1d4b98
http://hdl.handle.net/20.500.12278/35622

Formal Analysis of Ladder Programs using Deductive Verification

Autor: Lourenço, Cláudio, Cousineau, Denis, Faissole, Florian, Marché, Claude, Mentré, David, Inoue, Hiroaki

Publikováno v: [Research Report] RR-9402, Inria. 2021, pp.25

Programmable logic controllers (PLC) are industrial digital computers used as automation controllers of manufacturing processes, such as assembly lines or robotic devices. The Ladder language, also known as Ladder Logic, is a programming language use

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::c2b533e677c1c15eaff4516cd49f8421
https://hal.inria.fr/hal-03199464

Principles of program verification for arbitrary monadic effects

Autor: Kenji Maillard

Publikováno v: Programming Languages [cs.PL]. Université Paris sciences et lettres, 2019. English. ⟨NNT : 2019PSLEE081⟩
Computer Science [cs]. ENS Paris-Ecole Normale Supérieure de Paris, 2019. English
HAL

Computational monads are a convenient algebraic gadget to uniformly represent side-effects in programming languages, such as mutable state, divergence, exceptions, or non-determinism. Various frameworks for specifying programs and proving that they m

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::54dacb3e3da567e5028279df624333bd
https://tel.archives-ouvertes.fr/tel-03441023v2/document

A coverage combining tests and proofs for formal verification

Autor: Le, Viet Hoang

Actuellement, le développement d’un logiciel de taille industriel repose généralement surdes tests ou des preuves unitaires pour garantir rigoureusement ses exigences. En outre, il adéjà été montré que l’utilisation combinée du test et d

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=artemis___fr::cb265edda742a324958a0b5c707b6256
https://depozit.isae.fr/theses/2019/2019_Le_Viet-Hoang_D.pdf

Vérification automatique de programmes Ada effectuant des calculs en virgule flottante

Autor: Fumex, Clément, Marché, Claude, Moy, Yannick

Publikováno v: [Research Report] RR-9060, Inria Saclay Ile de France. 2017, pp.53

In critical software systems like the ones related to transport and defense, it is common toperform numerical computations implemented using floating-point arithmetic. Safety conditions for suchsystems typically require strong guarantees on the funct

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::cb3d9f20da1817cf061cf34581b306ea
https://inria.hal.science/hal-01511183/file/RR-9060.pdf