SOFTWARE ANALYSIS AND VERIFICATION
Learning outcomes of the course unit
The growing dependence of society on computer science
applications causes the analysis and verification of the
correctness of complex systems to increasingly represent
a critical factor of the development process.
The malfunctioning of systems, whether they are hardware,
software or communication protocols, can involve
considerable damage of every kind: from financial loss
to loss of human life. Also, when the defects are not
detected before the system is used,
the application of corrective measures is, when
possible, much more difficult and costly. Examples from the recent
past include the millennium bug, the errors
of some versions of the Pentium processor,
N.Y. Bank's 32 billion dollar overdraft,
the initial failure of the Ariane 5 carrier, and
the fatal accidents of the Therac-25.
The course intends to provide a first introduction to the
techniques that are at the basis of automatic software
analysis and computer assisted formal
Course contents summary
Introduction to software analysis and verification.
Program specifications and properties.
Floyd-Hoare logic and verification of the partial correctness of programs
Total correctness of programs and termination analysis.
Structured operational semantics.
Static program analysis.
G. Winskel, La semantica formale dei linguaggi di programmazione, UTET, 1999;
M. Gordon, Specification and Verication I (lecture notes), 2003.
G. Plotkin, A Structural Approach to Operational Semantics.
Individual or group project. Alternatively (for those who do not want to carry out a project), oral examination.