Co-inductive Axiomatization of a Synchronous ...
Document type :
Communication dans un congrès avec actes
DOI :
Title :
Co-inductive Axiomatization of a Synchronous Language
Author(s) :
Nowak, David [Auteur]
Environnement de programmation d'applications temps réel [EP-ATR]
Beauvais, Jean-René [Auteur]
Environnement de programmation d'applications temps réel [EP-ATR]
Talpin, Jean-Pierre [Auteur]
Environnement de programmation d'applications temps réel [EP-ATR]

Environnement de programmation d'applications temps réel [EP-ATR]
Beauvais, Jean-René [Auteur]
Environnement de programmation d'applications temps réel [EP-ATR]
Talpin, Jean-Pierre [Auteur]
Environnement de programmation d'applications temps réel [EP-ATR]
Conference title :
11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs '98)
City :
Canberra
Country :
Australie
Start date of the conference :
1998-09-27
Book title :
Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs '98
Publisher :
Springer-Verlag
Publication date :
1998
HAL domain(s) :
Informatique [cs]/Systèmes embarqués
English abstract : [en]
Over the last decade, the increasing demand for the validation of safety critical systems lead to the development of domain-specific programming languages (e.g. synchronous languages) and automatic verification tools (e.g. ...
Show more >Over the last decade, the increasing demand for the validation of safety critical systems lead to the development of domain-specific programming languages (e.g. synchronous languages) and automatic verification tools (e.g. model checkers). Conventionally, the verification of a reactive system is implemented by specifying a discrete model of the system (i.e. a finite-state machine) and then checking this model against temporal properties (e.g. using an automata-based tool). We investigate the use of a theorem prover, Coq, for the specification of infinite state systems and for the verification of co-inductive properties.Show less >
Show more >Over the last decade, the increasing demand for the validation of safety critical systems lead to the development of domain-specific programming languages (e.g. synchronous languages) and automatic verification tools (e.g. model checkers). Conventionally, the verification of a reactive system is implemented by specifying a discrete model of the system (i.e. a finite-state machine) and then checking this model against temporal properties (e.g. using an automata-based tool). We investigate the use of a theorem prover, Coq, for the specification of infinite state systems and for the verification of co-inductive properties.Show less >
Language :
Anglais
Peer reviewed article :
Oui
Audience :
Internationale
Popular science :
Non
Collections :
Source :
Files
- https://hal.archives-ouvertes.fr/hal-00544505/document
- Open access
- Access the document
- https://hal.archives-ouvertes.fr/hal-00544505/document
- Open access
- Access the document
- document
- Open access
- Access the document
- TPHOLs-98_sem_verif.pdf
- Open access
- Access the document
- TPHOLs-98_sem_verif.pdf
- Open access
- Access the document
- document
- Open access
- Access the document
- TPHOLs-98_sem_verif.pdf
- Open access
- Access the document