1
00:00:00,280 --> 00:00:02,750
So let me start with some examples that motivate the

2
00:00:02,750 --> 00:00:06,330
need for very fine software. The first example I want to

3
00:00:06,330 --> 00:00:09,580
use is the famous Arian five. And if you remember

4
00:00:09,580 --> 00:00:13,060
that's a rocket that exploded not too long after departure.

5
00:00:13,060 --> 00:00:15,800
Because of a software error. And even without going to

6
00:00:15,800 --> 00:00:19,400
such dramatic examples. I'm sure you're all familiar with this

7
00:00:19,400 --> 00:00:22,470
kind of situation. Or this one, or again in this

8
00:00:22,470 --> 00:00:26,070
one. And here I'm not really picking on any specific organization,

9
00:00:26,070 --> 00:00:32,280
operating system or software. The point I want to make is that software is

10
00:00:32,280 --> 00:00:34,730
buggy. In fact, a federal report from

11
00:00:34,730 --> 00:00:37,810
a few years ago assessed that software bugs

12
00:00:37,810 --> 00:00:41,300
are costing the US economy, $60 billion

13
00:00:41,300 --> 00:00:44,120
every year. In addition, studies have shown that

14
00:00:44,120 --> 00:00:47,810
software contains on average one to five

15
00:00:47,810 --> 00:00:51,472
bugs every 1000 lines of code. Building 100%

16
00:00:51,472 --> 00:00:55,940
correct mass-market software is just impossible. And if

17
00:00:55,940 --> 00:00:58,270
this is the case, what can we do?

18
00:00:58,270 --> 00:01:03,520
What we need to do is to verify software as much as possible. In this part of

19
00:01:03,520 --> 00:01:05,750
the course, we will discuss how we can

20
00:01:05,750 --> 00:01:09,480
do this. We will discuss different alternative ways

21
00:01:09,480 --> 00:01:13,980
of very fine software systems. With particular attention

22
00:01:13,980 --> 00:01:16,570
to the most common type of verification. Which is

23
00:01:16,570 --> 00:01:19,470
software testing. Before doing that however, let

24
00:01:19,470 --> 00:01:21,090
me go over some basic terms that are

25
00:01:21,090 --> 00:01:23,190
commonly used. And I have to say,

26
00:01:23,190 --> 00:01:26,330
often misused in the context of software verification.