|
Learning outcomes |
This course addresses the concepts, the methodologies and tools that allow for the design of reliable (mathematically sound) applications, on an industrial scale.
Upon completion of the course, the students should be able to:
- study the different aspects of reliability
- Choose the appropriate technology, formalism and tools for a specific realiable software project.
- Modeling, implementing reliable systems
- Certify, that is prove with the help of the computer reliability results.
|
|
Syllabus |
From a theoretical point of view, this course introduces the mathematical models upon which it is possible to compute and reason about programs.
In its practical component, the course introduces how to design and use models of programs, how to test and verify correctness properties, before proceeding to the implementation stage and in order to avoid errors or bugs. In short: model, calculate, verify, test and evaluate.
|
|
Main Bibliography |
José Carlos Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa. Rigorous Software Development, An Introduction to Program Verification. Series: Undergraduate Topics in Computer Science, Springer. 1st Edition., 2011, XIII, 307 p. 52 illus. ISBN: 978-0-85729-017-5.
Development An Introduction to Program Verification. Springer Verlag, 2010.
Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development. Springer Verlag, 2004.
J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.
Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, and Philippe Schnoebelen. Systems and Software Verification. Model-Checking Techniques and Tools. Springer, 2001.
J-F. Monin. Understanding Formal Methods. Springer Verlag, 2002. Translation editor M. Hinchey.
H. R. Nielson, F. Nielson, and C. L. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.
|