Introduction to software verification via model checking.
I have found a nice set of lecture on software verification:

The course introduces the theory and practice of formal methods for the design and analysis of software systems. The course will cover the underlying logical and theoretical concepts, with focus on the algorithmic solutions, and heuristics to cope with the high computational complexity.
Unfortunately, I cannot embed videos in the post, so I will just provide links to the videolectures:
http://www.lektorium.tv/lecture/?id=12941
http://www.lektorium.tv/lecture/?id=12942
Proving the Eisenstein’s criteria
Polynomial , where each
is divisible by some number
, is irreducible in
when
does not divide
.
If A is not irreducible then there are some and
such as
.
But that means that , which means that
XOR
(since
does not divide
).
Let’s assume that . Now let’s take a map
(I believe this method is called homomorphism-reduction).
, but
, where
.
That is possible only when is constant and
. Which means that
is irreducible.
Note: here denotes
where
is a homomorphism
.
Union of countable sets is countable.
Let’s say we have a possibly infinite collection of countable sets , prove that
is countable too. We are going to do this using Axiom of Choice.
Since every set is countable, there is a set of injections from
to
, let’s call it
. Using the axiom of choice we can create a set of maps
from
to
. Now, we are going to create an injection from
to
. If
is an element of
then it’s also an element of some set
. Therefore we can construct
where
. And since we know that
is countable, we can map
to
. QED.