Learning objectives
<span class="datirigaalto"><span class="datirigaalto">The growing dependence of society on computer science<br />
applications causes the analysis and verification of the<br />
correctness of complex systems to increasingly represent<br />
a critical factor of the development process.<br />
The malfunctioning of systems, whether they are hardware,<br />
software or communication protocols, can involve<br />
considerable damage of every kind: from financial loss<br />
to loss of human life. Also, when the defects are not <br />
detected before the system is used,<br />
the application of corrective measures is, when<br />
possible, much more difficult and costly. Examples from the recent<br />
past include the millennium bug, the errors<br />
of some versions of the Pentium processor,<br />
N.Y. Bank's 32 billion dollar overdraft,<br />
the initial failure of the Ariane 5 carrier, and<br />
the fatal accidents of the Therac-25.<br />
<br />
The course intends to provide a first introduction to the<br />
techniques that are at the basis of automatic software<br />
analysis and computer assisted formal<br />
verification. </span></span>