Reference : Automates et vérification
Parts of books : Contribution to collective works
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/12421
Automates et vérification
French
Wolper, Pierre mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique (parallélisme et banques de données) >]
Dec-2006
Encyclopédie de l'informatique et des systèmes d'information
Vuibert
977--986
2-7117-4846-4
Paris
[en] finite automata ; verification ; concurrent programs ; temporal logic
[en] La vérification de programmes consiste à analyser les comportements possibles de programmes
en vue de déterminer s’ils seront toujours conformes à ce qui est attendu. Pour ce
faire, les caractéristiques souhaitées des comportements sont exprimées formellement et confrontées,
par des techniques mathématiques rigoureuses, à l’ensemble des comportements du
programme à analyser. Dans ce contexte, les automates jouent un triple rôle. Tout d’abord, ils
sont fréquemment utilisés en tant que langage de programmation simplifié pour décrire les programmes
à analyser. Ensuite, ils servent de formalisme de description de propriétés de comportements,
soit directement, soit par traduction à partir d’un langage logique. Finalement, ils
s’avèrent très utiles en tant que formalisme de description d’ensembles infinis de valeurs.
Professionals
http://hdl.handle.net/2268/12421

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Restricted access
epreuves4-10.pdfAuthor preprint399.09 kBRequest copy

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.