BSP-Why, un outil pour la vérification déductive de programmes BSP : machine-checked semantics and application to distributed state-space algorithms
This thesis takes part in the formal verification of parallel programs. The aim of formal verification is to ensure that a program will run as it should, without making mistakes, blocking, or terminating abnormally. This is even more important in the parallel computation field, where the cost of cal...
Main Author: | Fortin, Jean |
---|---|
Language: | English |
Published: |
Université Paris-Est
2013
|
Subjects: | |
Online Access: | http://tel.archives-ouvertes.fr/tel-00974977 http://tel.archives-ouvertes.fr/docs/00/97/49/77/PDF/TH2013PEST1084_complete.pdf |
Similar Items
-
Synthesis of correct-by-design schedulers for hybrid systems
by: Soulat, Romain
Published: (2014) -
BSP-Why, un outil pour la vérification déductive de programmes BSP : machine-checked semantics and application to distributed state-space algorithms
by: Fortin, Jean
Published: (2013) -
Verification and composition of security protocols with applications to electronic voting
by: Ciobâcǎ, Ştefan
Published: (2011) -
Separation logic : expressiveness, complexity, temporal extension
by: Brochenin, Rémi
Published: (2013) -
Hybrid and Anonymous File-Sharing Environments: Architecture and Characterisation
by: Timpanaro, Juan Pablo
Published: (2013)