Wed, Jan 8th
Lecture 2 - What is software verification?
Does it do what it need to do?
Did we write the right code?
Static vs Dynamic
a. look for errors
b. prove that it behaves as described in specifications
• You can make sure something works as expected. And because it is that well accurate, it
takes time to do it, and you have the option of using unit levels for the big codes.
• Static means that you are not executing the code.
• It's effective and trusted
• You can use model checking, data-flow analysis, abstraction interpretation, assertion based
• You work with the code, and it is executing
Why do we test?
• Its not possible to check all mistakes duing the process, so after they are ready you need to
check it before the user does
Software is design with a purpose. Its an engineered product. Its does what the specifications
describe. And there is a ISO for it.
- how well does it work?
- what methods does it have?
Types of testing:
Black Box Testing
• Assume you dont know what is in the software.
• You know what it is supposed to do but not how it does what it does.
• You need to make sure to know what is that you need to input in order to get the right
• It can be used on any size of code. • If there is a requirement that is not satisfied, you know what requirement is the wrong
• Good to test specifications!
White Box Testing
• You can see whats inside the code
• Time consuming because you can/have to read the code
• Better with small code
• Can use sudo code, a flow charge, that takes the logic out of the code and test what that is
supposed to do.
OBS: Coverage example on the notes is dynamic.
Degree of coverage
• When can you say that you have tested enough?
• Degree of coverage - how much was tested in the software
• decision , sometimes a decision is to be made and it leads to branches.
• What is false is false at least once, and the same goes for true
• Path coverage - you need to test every possible combination
From Static Analysis
• Unit Testing
◦ this is for q