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 focuses on these recent research results, though it also covers fundamentals of verification and includes a “bootcamp” tour of multiple verification tools.