Výsledky vyhledávání - "Alexandre, Francis"

Raffinement B de systèmes de transitions étiquetés

Autor: Mouakher, Inès, Alexandre, Francis

Publikováno v: [Rapport de recherche] 2009, pp.37

Le raffinement est une notion clé dans la méthode B. Nous étudions le rapport entre cette notion et certaines relations entre systèmes de transitions étiquetés telles que la simulation, la bisimulation... Le point de départ de l'étude est la

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::49c5d60d7460043eba32e935bb80b693
https://inria.hal.science/inria-00435896

Zobrazit plný text záznamu

Protocol verification in a software component approach

Autor: Mouakher, Inès, Alexandre, Francis, Souquières, Jeanine

Component based software development approaches represent an important challenge for the integration of formal methods into engineering development processes. In these approaches, components are considered as black boxes communicating through require

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od_______166::f256b11056ac9cf5b3ae40334555858e
https://hal.archives-ouvertes.fr/hal-00182262

Zobrazit plný text záznamu

Automatisation de l'application de l'hypothèse de récurrence dans la preuve des formules implicatives

Autor: Mouakher, Inès, Alexandre, Francis, Bsaïes, Khaled

Publikováno v: Premières Journées Francophones de Programmation par Contraintes-JFPC'2005
Premières Journées Francophones de Programmation par Contraintes-JFPC'2005, CRIL-CNRS FRE 2499, Jun 2005, Lens/France, pp.179-188

http://www710.univ-lyon1.fr/~csolnon; L'objectif général de ce travail est de prouver les propriétés des programmes logiques (ensemble de clauses de Horn). Ces propriétés sont des formules de la forme A

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

Zobrazit plný text záznamu

Proving Theorems by Folding/Unfolding

Autor: Demba, Moussa, Bsaïes, Khaled, Alexandre, Francis

Publikováno v: 2nd International Conference : Sciences of Electronic, Technologies of Information and Telecommunications-SETIT 2004
2nd International Conference : Sciences of Electronic, Technologies of Information and Telecommunications-SETIT 2004, Mar 2004, Sousse, Tunisie, 6 p

Colloque avec actes et comité de lecture. internationale.; International audience; Proofs techniques can be seen as simplification methods, i.e. formulas are transformed into trivial ones, true. Unfortunately, we are sometimes faced with an unprovab

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

Zobrazit plný text záznamu

A Method for Patching Faulty Conjectures

Autor: Demba, Moussa, Alexandre, Francis, Bsaïes, Khaled

Publikováno v: [Intern report] A04-R-321 || demba04a, 2004, 20 p

Rapport interne.; We present a method for patching faulty conjectures in automatic theorem proving. The method is based on well-known folding/unfolding deduction rules. The conjectures we are interested in here are implicative formulas that are of th

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

Zobrazit plný text záznamu

Correction de conjectures fausses par synthèse de programmes

Autor: Demba, Moussa, Alexandre, Francis, Bsaïes, Khaled

Publikováno v: Douzièmes Journées Francophones de Programmation Logique et Programmation par Contraintes 2003-JFPLC'2003
Douzièmes Journées Francophones de Programmation Logique et Programmation par Contraintes 2003-JFPLC'2003, 2003, Amiens, France, 4 p

Colloque avec actes et comité de lecture. internationale.; International audience; Dans le domaine de la vérification, les preuves ne terminent pas toujours avec succès, à cause des formules non prouvables. Parfois, le prouveur signale simplement

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

Zobrazit plný text záznamu

Correction de conjectures faussses

Autor: Demba, Moussa, Alexandre, Francis, Bsaïes, Khaled

Publikováno v: [Interne] A02-R-492 || demba02a, 2002

Rapport interne.; Dans le domaine de la vérification, les preuves se terminent souvent par des formules fausses ou non prouvables. En général, le prouveur signale simplement l'échec. Cependant, dans certains cas il est intéressant de connaître

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

Zobrazit plný text záznamu

Preuves par récurrence : stratégies et résultats de décidabilité

Autor: Alexandre, Francis

Publikováno v: [Interne] A02-R-489 || alexandre02c, 2002

Rapport interne.; Nous présentons des stratégies pour prouver des formules implicatives. L'objectif principal est de prouver qu'une formule implicative est valide dans le plus petit modèle de Herbrand d'un programme défini donné. Les stratégies

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::a47afb4a7cd1386cde0bffd32ca19b9d
https://inria.hal.science/inria-00101077

Zobrazit plný text záznamu

Stratégies de preuves par récurrence basées sur le pliage et le dépliage

Autor: Alexandre, Francis, Demba, Moussa, Bsaïes, Khaled

Publikováno v: [Interne] A01-R-284 || alexandre01b, 2001, 14 p

Rapport interne.; Nous présentons des stratégies de preuves de formules implicatives. Etant donné un programme (ensemble de clauses de Horn), l'objectif général est de démontrer qu'une formule implicative est vraie dans le plus petit modèle de

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

Zobrazit plný text záznamu

Pliage et récurrence pour le construction de programme

Autor: Alexandre, Francis, Bsaïes, Khaled

Publikováno v: [Interne] A00-R-382 || alexandre00e, 2000, 10 p

Rapport interne.; Dans le cadre de la construction de programmes par transformation ou par synthese, le probleme de la preuve des formules implicatives est fondamental. Les principes de recurrence jouent un role essentiel et central dans les prouveur

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

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání