Software verification is the application of rigorous mathematical techniques
to prove that computer programs do what they are supposed to.  The
conventional approach to software development uses testing to give assurance
of correctness.  But while testing finds many bugs, it's always possible for
some to make it to released software.  When the cost of bugs can be measured
in millions of dollars, or even human lives, the benefit of verification --
which guarantees the absence of bugs -- is apparent.

In this talk, we will address a particular challenge to software verification:
concurrency.  Threads in a concurrent program can operate on the same data
simultaneously.  Such behaviour is tricky to reason about.  We will look at
classic approaches to this (the Owicki-Gries and Rely-Guarantee methods), and
more recent approaches based on separation logic.  We will see how these
approaches emphasise appropriate abstractions that simplify the reasoning
required to verify sophisticated concurrent algorithms