-
1تقرير
المؤلفون: Cousineau, Denis, Inoue, Hiroaki, Marché, Claude, Mentré, David
المساهمون: Mitsubishi Electric R&D Centre Europe France (MERCE-France), Mitsubishi Electric France, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Inria
المصدر: https://inria.hal.science/hal-04487766Test ; RT-0522, Inria. 2024.
مصطلحات موضوعية: Ladder Language for PLCs, Formal Specification, Why3 Environment for Deductive Verification, Model Validation, langage Ladder pour les PLC, Spécification formelle, environnement Why3 pour la vérification déductive, Validation de modèle, [INFO]Computer Science [cs]
العلاقة: Report N°: RT-0522; hal-04487766; https://inria.hal.science/hal-04487766Test; https://inria.hal.science/hal-04487766/documentTest; https://inria.hal.science/hal-04487766/file/RT-0522.pdfTest
-
2تقرير
المساهمون: Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Mitsubishi Electric R&D Centre Europe France (MERCE-France), Mitsubishi Electric France, TrustInSoft (TIS ), Inria
المصدر: https://inria.hal.science/hal-04343157Test ; RR-9531, Inria. 2023.
مصطلحات موضوعية: Formal specification, Deductive verification, Why3 environment, Floating-point computations, Spécification formelle, preuve de programmes, environnement Why3 pour la vérification déductive, programmes C en virgule flottante, [INFO]Computer Science [cs]
العلاقة: Report N°: RR-9531; hal-04343157; https://inria.hal.science/hal-04343157Test; https://inria.hal.science/hal-04343157v2/documentTest; https://inria.hal.science/hal-04343157v2/file/RR-9531v2.pdfTest
-
3تقرير
المؤلفون: Denis, Xavier, Jourdan, Jacques-Henri, Marché, Claude
المساهمون: Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Inria Saclay - Île de France
المصدر: https://inria.hal.science/hal-03526634Test ; [Research Report] RR-9448, Inria Saclay - Île de France. 2021.
مصطلحات موضوعية: Rust programming language, Formal Specification, Deductive verification, Aliasing and Ownership, Prophecies, Traits, Langage de programmation Rust, Spécification formelle, Vérification Déductive, Alias, Ownership, Prophéties, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
العلاقة: Report N°: RR-9448; hal-03526634; https://inria.hal.science/hal-03526634Test; https://inria.hal.science/hal-03526634v2/documentTest; https://inria.hal.science/hal-03526634v2/file/report.pdfTest
-
4تقرير
المؤلفون: Lourenço, Cláudio, Cousineau, Denis, Faissole, Florian, Marché, Claude, Mentré, David, Inoue, Hiroaki
المساهمون: Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Mitsubishi Electric R&D Centre Europe France (MERCE-France), Mitsubishi Electric France, Mitsubishi Electric Corporation, This work has been partially supported by the bilateral contract ProofInUse-MERCE between Inria team Toccata and Mitsubishi Electric R&D Centre Europe, Rennes., Inria
المصدر: https://inria.hal.science/hal-03199464Test ; [Research Report] RR-9402, Inria. 2021, pp.25.
مصطلحات موضوعية: Formal specification, Deductive verification, Ladder language for programming PLCs, Why3 environment for deductive verification, Spécification formelle, Preuve de programmes, Langage Ladder pour la programmation des PLC, Environnement Why3 pour la vérification déductive, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
العلاقة: Report N°: RR-9402; hal-03199464; https://inria.hal.science/hal-03199464Test; https://inria.hal.science/hal-03199464/documentTest; https://inria.hal.science/hal-03199464/file/RR-9402.pdfTest
-
5تقرير
المؤلفون: Becker, Benedikt, Belo Lourenço, Cláudio, Marché, Claude
المساهمون: Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), This work has been partially supported by the bilateral contract ProofInUse-AdaCore between Inria team Toccata and AdaCore company, Paris, France, and by the bilateral contract ProofInUse-MERCE between Toccata and Mitsubishi Electric R&D Centre Europe, Rennes, France., Inria
المصدر: https://inria.hal.science/hal-03213438Test ; [Research Report] RR-9407, Inria. 2021, pp.43.
مصطلحات موضوعية: Formal Specification, Deductive Verification, Generation of counterexamples, Runtime assertion checking, Program Verifier Why3, Spécification formelle, preuve de programmes, génération de contre-exemples, vérification d'assertions à l'exécution, Environnement de preuve Why3, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
العلاقة: Report N°: RR-9407; hal-03213438; https://inria.hal.science/hal-03213438Test; https://inria.hal.science/hal-03213438/documentTest; https://inria.hal.science/hal-03213438/file/RR-9407.pdfTest
-
6رسالة جامعية
المؤلفون: Bougacha, Racem
المساهمون: Évaluation des Systèmes de Transports Automatisés et de leur Sécurité (COSYS-ESTAS ), Université Gustave Eiffel, Centrale Lille Institut, Simon Collart-Dutilleul, Régine Laleau
المصدر: https://theses.hal.science/tel-04412845Test ; Other [cs.OH]. Centrale Lille Institut, 2023. English. ⟨NNT : 2023CLIL0014⟩.
مصطلحات موضوعية: High level architecture, Requirement, Alignment, SysML/KAOS - SysML, Model transformation, Formal specification, Event-B Method, Architecture de haut niveau, Exigence, Alignement, Transformation de modèles, Spécification formelle, Méthode Event -B, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH]
العلاقة: NNT: 2023CLIL0014; tel-04412845; https://theses.hal.science/tel-04412845Test; https://theses.hal.science/tel-04412845/documentTest; https://theses.hal.science/tel-04412845/file/Bougacha_Racem_DLE.pdfTest
-
7رسالة جامعية
المؤلفون: Bougacha, Racem
المساهمون: Centrale Lille Institut, Collart-Dutilleul, Simon, Laleau, Régine
-
8مؤتمر
المساهمون: DGA Maîtrise de l'information (DGA.MI), Direction générale de l'Armement (DGA), Diversity-centric Software Engineering (DiverSe), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Catherine Dubois, Dominique Mery, Paolo Masci
المصدر: Electronic Proceedings in Theoretical Computer Science (EPTCS) ; 3rd Workshop on Formal Integrated Development Environment ; https://hal.inria.fr/hal-01401849Test ; 3rd Workshop on Formal Integrated Development Environment, Catherine Dubois; Dominique Mery; Paolo Masci, Nov 2016, Limassol, Cyprus ; https://sites.google.com/site/fideworkshop2016Test/
مصطلحات موضوعية: Formal specification, Language, Semantics, Packet filtering, K framework, Spécification Formelle, Langage, Sémantique, Filtrage de trames, Framework K, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], [INFO.INFO-IA]Computer Science [cs]/Computer Aided Engineering
العلاقة: hal-01401849; https://hal.inria.fr/hal-01401849Test; https://hal.inria.fr/hal-01401849/documentTest; https://hal.inria.fr/hal-01401849/file/2016-08-21_F-IDE_FSPFL.pdfTest
-
9دورية أكاديمية
المؤلفون: Bonnet, Grégory, Mermet, Bruno, Simon, Gaële
المساهمون: Equipe MAD - Laboratoire GREYC - UMR6072, Groupe de Recherche en Informatique, Image et Instrumentation de Caen (GREYC), Université de Caen Normandie (UNICAEN), Normandie Université (NU)-Normandie Université (NU)-École Nationale Supérieure d'Ingénieurs de Caen (ENSICAEN), Normandie Université (NU)-Centre National de la Recherche Scientifique (CNRS)-Université de Caen Normandie (UNICAEN), Normandie Université (NU)-Centre National de la Recherche Scientifique (CNRS)
المصدر: ISSN: 0992-499X ; EISSN: 1958-5748.
مصطلحات موضوعية: formal specification, multi-agent systems, formal specification, ethic, computational ethics, spécification formelle, Systèmes multi-agents SMA, éthique computationelle, ACM: I.: Computing Methodologies/I.2: ARTIFICIAL INTELLIGENCE, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], [INFO.INFO-MA]Computer Science [cs]/Multiagent Systems [cs.MA]
العلاقة: hal-01705240; https://hal.science/hal-01705240Test; https://hal.science/hal-01705240/documentTest; https://hal.science/hal-01705240/file/ria2016PourHAL2.pdfTest
الإتاحة: https://doi.org/10.3166/ria.31.449-470Test
https://hal.science/hal-01705240Test
https://hal.science/hal-01705240/documentTest
https://hal.science/hal-01705240/file/ria2016PourHAL2.pdfTest -
10تقرير
المؤلفون: Fumex, Clément, Marché, Claude, Moy, Yannick
المساهمون: Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), AdaCore (FRANCE), Inria Saclay Ile de France, ANR-14-LAB3-0007,ProofInUse,Preuve en Œuvre (Intégration de la preuve dans le développement logiciel)(2014), ANR-14-CE28-0020,SOPRANO,Nouveau prouveur automatique pour l'analyse de programmes(2014)
المصدر: https://inria.hal.science/hal-01511183Test ; [Research Report] RR-9060, Inria Saclay Ile de France. 2017, pp.53.
مصطلحات موضوعية: Formal Specification, Deductive Verification, Formal Proof, Program Verifiers Why3 and SPARK, Floating-point computations, Spécification formelle, preuve de programmes, environnements de preuve Why3 et SPARK, calculs en virgule flottante, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-AO]Computer Science [cs]/Computer Arithmetic
العلاقة: Report N°: RR-9060; hal-01511183; https://inria.hal.science/hal-01511183Test; https://inria.hal.science/hal-01511183/documentTest; https://inria.hal.science/hal-01511183/file/RR-9060.pdfTest
