Beware of bugs in the above code; I have only proved it correct, not tried it.
- Donald Knuth
As the world increasingly depends on software, to control our finances, drive our cars, and manage our medical devices, how can we tell whether that software will be correct, secure, or reliable? Testing for such properties is notoriously difficult and ineffective. Software verification can, in principle, provide such guarantees, but verification has historically been difficult to apply at scale. A recent series of results, however, suggests we may be at an inflection point, as various research groups have successfully proven rigorous properties about critical software components, including OS kernels, compilers, cryptographic libraries, and distributed systems.
15-811 will focus on these recent research results, though it will also cover fundamentals of verification and include a “bootcamp” tour of multiple verification tools.