Une aide à la réutilisation de preuves formelles : application aux preuves de propriétés sémantiques |
|
Analyse de dépendances ML pour les évaluateurs de logiciels critiques. |
|
Analyse et spécification formelle des systèmes d'enclenchement ferroviaire basés sur les relais |
|
Analysis and formal specification of relay-based railway interlocking systems. |
|
Apprentissage de la programmation avec OCaml |
|
Une approche formelle pour la substitution correcte par construction de systèmes. |
|
Approches formelles pour le développement de logiciels : [actes des 12e et 13e éditions de l'atelier AFADL, 2013, Nancy et 2014, Paris] |
|
Assisted concurrent program verification by code and specification transformation. |
|
Automatic testing of properties in a safe software development framework. |
|
Bibliothèque certifiée en Coq pour la provenance des données |
|
Bounded domain property for first order linear temporal logic and applications to the verification of infinite-state systems. |
|
Calculer avec des relations, des fonctions et des lieurs. |
|
Certification de programmes avec des effets calculatoires |
|
Certification of programs with computational effects. |
|
Certified algorithms for program slicing |
|
Classification de menaces d'erreurs par analyse statique, simplification syntaxique et test structurel de programmes |
|
Classification of errors threats by static analysis, program sclicing and structural testing of programs. |
|
Computing with relations, functions, and bindings |
|
Construction de Logiques-Objet Sémantiquement Correct pour des Langages à Domaines Spécifiques Basés sur UML/OCL. |
|
Contribution to software verification combining tests and proofs. |
|
A Coq certified library for data provenance. |
|
Coupling of formal methods for industriel systems specification. |
|
Une couverture combinant tests et preuves pour la vérification formelle |
|
Démarche de conception formelle pour systèmes mécatroniques critiques automobiles. |
|
Développement de la programmation par tuilage pour les systèmes multimédias interactifs |
|
Développement de logiciels corrects par construction à partir de lignes de produits. |
|
Développement et vérification de bibliothèques d'arithmétique entière en précision arbitraire. |
|
Encodages de la théorie des ensembles de TLA⁺ pour la preuve automatique. |
|
Encoding TLA⁺'s Set Theory for Automated Theorem Provers |
|
Un environnement formel pour la sémantique des systèmes hétérogènes. |
|
[ErgoFast] Improving performance of the SMT solver Alt-Ergo with a better integration of efficient SAT solver. |
|
Etude de l'application de gestion commerciale et comptable |
|
Extraction of Certified Functional Code from Inductive Specifications. |
|
Fastest : amélioration et développement du Test Template Framework. |
|
Fastest : improving and supporting the Test Template Framework |
|
Formal methods meet Security in a Cost Efficient Cloud Brokerage Security. |
|
Formalisation du temps et de la causalité dans les modèles polychrones polytemporisés. |
|
Formalizing Time and Causality in Polychronous Polytimed Models |
|
From natural language specifications to formal specifications via an ontology as a pivot model. |
|
Functional abstraction for programming multi-level architectures : formalisation and implementation. |
|
A help with the reuse of formal proofs application to the proofs of semantic properties. |
|
I hume you : novel with exercices : self study edition with answers : a novel method of improving your basic English laguage skills : [story with exercises and answers] |
|
JFLA 2000 : [actes des 11e] Journées francophones des langages applicatifs, Le Mont Saint-Michel, 31 janvier-1er février 2000 |
|
Mécanismes orientés objet pour l’interopérabilité entre systèmes de preuve. |
|
A meta-approach to describe effectful and distributed semantics |
|
Une méta-approche pour décrire des sémantiques distribuées et avec effets. |
|
Methodes formelles et Sécurité en informatique en nuages |
|
Méthodes formelles pour la modélisation géométrique à base topologique : définitions et algorithmes avec la méthode B |
|
Méthodes pour le raisonnement d'ordre supérieur dans SMT |
|
Methods for Higher-Order reasoning in SMT. |
|
Modélisation UML/B pour la validation des exigences de sécurité des règles d'exploitation ferroviaires |
|
New techniques for instantiation and proof production in SMT solving. |
|
Nouvelles techniques pour l'instanciation et la production des preuves dans SMT |
|
Object-Oriented Mechanisms for Interoperability Between Proof Systems |
|
Ontology centric design process : Sharing a conceptualization |
|
Optimisation du code source pour les systèmes critiques de sécurité. |
|
Optimization of source code for safety-critical systems |
|
Outils et techniques pour la vérification de programmes impératives modulaires. |
|
Preuves par raffinement de programmes avec pointeurs |
|
Proof Automation for Atelier B Rules Verification. |
|
Proofs by refinement of programs with pointers. |
|
Propriété du domaine borné pour la logique temporelle linéaire du premier ordre et applications à la vérification de systèmes à états infinis |
|
ROLE DU SYSTEME IGF (INSULIN-LIKE GROWTH FACTOR) DANS LA MYOGENESE : ETUDE DES VOIES DE SIGNALISATION CONTROLANT L'EXPRESSION D'IGFBP-5 (IGF BINDING PROTEIN-5) |
|
Safe control of obfuscation toolchains. |
|
Support for the validation and verification of critical systems : ontologies and integration of components. |
|
Test automatique de propriétés dans un atelier de développement de logiciels sûrs |
|
Test generation and animation based on object-oriented specifications |
|
Tests and Proofs : Third International Conference, TAP 2009, Zurich, Switzerland, July 2-3, 2009 : Proceedings |
|
Tools and Techniques for the Verification of Modular Stateful Code |
|
UML/B modeling for the safety requirements validation of railway operating rules. |
|
Vérification automatisée de certificats de terminaison. |
|
Vérification de spécifications modales de réseaux worklows à l'aide de solveurs de contraintes et de methodes de résolution. |
|
Vérification des résultats de l'inférence de types du langage OCaml |
|
Verification formelle et optimisation de l'allocation de registres |
|
Verified information flow control applied to cyber-physical systems. |
|
Verifying Modal Specifications of Workflow Nets : using Constraint Solving and Reduction Methods |
|