|
|
Teaching-CSC4504 for Dr J. Paul Gibson, LOgiciels-Réseaux (LOR), T&MSP SudParis, France. |
This course is a key component of the module Langages Formels et Applications . The course can be taught in English and French. In 2010, the chosen teaching language is English
The main objectives of this course are to learn about the use of formal specification in the development of software, and to be able to verify development steps using a theorem prover. The secondary objectives are for you to be able to develop and verify code more rigorously/formally using design-by-contract techniques.
The chosen formal modelling language is Event-B. However, participants will also be presented with OO designs (in UML) and OO code (in Java).
The teaching approach is Problem-Based Learning , which emphasises learning through doing.
Formal verification of tamper-evident storage for e-voting,
Dominique Cansell,
Gibson, J. Paul, and Dominique Méry,
in
Proceedings of
5th IEEE International Conference on
Software Engineering and Formal Methods
(SEFM07),
London, 10-14 September 2007.
Published by
IEEE Computer Science Press, pages 329-338, isbn = 0-7695-2884-8, editors Mike Hinchey and Tiziana Margaria.
Refinement: a constructive approach to formal software design for a secure e-voting
interface,
Dominique Cansell,
Gibson, J. Paul, and Dominique Méry.
Electronic Notes in Theoretical Computer Science, 183 (2007), pages 39–55,
Elsevier,
ISSN 1571-0661.
DOI: 10.1016/j.entcs.2007.01.060.
|
URL: http://www-public.it-sudparis.eu/~gibson/Teaching/CSC4504/ |
Last Revision: 8th March 2010 |
Contact: paul.gibson@it-sudparis.eu |