-
Proofs by refinement of programs with pointers
The purpose of this thesis is to specify and prove programs with pointers, such as C programs, using refinement techniques. The proposed approach allows a compromise... -
BSP-Why, un outil pour la vérification déductive de programmes BSP : machine-...
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...
