L'assistant à la démonstration Coq: application à la preuve de systèmes parallèles / The Coq proof assistant : parallel systems application

PAULIN-MOHRING, C

In: MOVEP '98 : modélisation et vérification des processus parallèles (Nantes, 6-9 juillet 1998) :239-251

Konferenz - print, 19 ref

Ces notes sont une introduction à l'assistant à la démonstration Coq, elles présentent le langage de spécifications ainsi que l'architecture du système de preuves. Elles illustrent ensuite l'utilisation de ce langage pour la modélisation et la preuve de systèmes parallèles en étudiant la sémantique d'un mini-langage de commandes gardées et en modélisant un algorithme simple d'exclusion mutuelle. Les exemples présentés ici ont été développés en utilisant la version V6.2 du manuel. Le lecteur pourra consulter le manuel de référence [1] pour des informations plus précises sur les différentes constructions.

Titel:	L'assistant à la démonstration Coq: application à la preuve de systèmes parallèles / The Coq proof assistant : parallel systems application
Autor/in / Beteiligte Person:	PAULIN-MOHRING, C
Link:	View record from PASCAL Archive
Quelle:	MOVEP '98 : modélisation et vérification des processus parallèles (Nantes, 6-9 juillet 1998) :239-251
Veröffentlichung:	1998
Medientyp:	Konferenz
Umfang:	print, 19 ref
Schlagwort:	Computer science Informatique Sciences exactes et technologie Exact sciences and technology Sciences appliquees Applied sciences Informatique; automatique theorique; systemes Computer science; control theory; systems Logiciel Software Systèmes informatiques et systèmes répartis. Interface utilisateur Computer systems and distributed systems. User interface Simulation système System simulation Simulación sistema Système informatique Computer system Sistema informático Système parallèle Parallel system Sistema paralelo Vérification formelle Formal verification Vérification programme Program verification Verificación programa
Sonstiges:	Nachgewiesen in: PASCAL Archive Sprachen: French Original Material: INIST-CNRS Document Type: Conference Paper File Description: text Language: French Author Affiliations: LRI-URA 410 du CNRS, Université Paris Sud-Bat 490, 91405 Orsay, France Rights: Copyright 1999 INIST-CNRS ; CC BY 4.0 ; Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS Notes: Computer science; theoretical automation; systems

Klicken Sie ein Format an und speichern Sie dann die Daten oder geben Sie eine Empfänger-Adresse ein und lassen Sie sich per Email zusenden.

BibTeX Citavi, JabRef, u.a.
(Literaturverwaltung)

PDF kein Volltext!
(Merkzettel, Notizen)

RIS Endnote, Citavi u.a.
(Literaturverwaltung)

MODS
(XML zur Weiterverarbeitung)

oder

Wählen Sie das für Sie passende Zitationsformat und kopieren Sie es dann in die Zwischenablage, lassen es sich per Mail zusenden oder speichern es als PDF-Datei.

Gewünschter Zitations-Stil:

oder

Bitte prüfen Sie, ob die Zitation formal korrekt ist, bevor Sie sie in einer Arbeit verwenden. Benutzen Sie gegebenenfalls den "Exportieren"-Dialog, wenn Sie ein Literaturverwaltungsprogramm verwenden und die Zitat-Angaben selbst formatieren wollen.