An Axiomatic Basis for Computer Programming by C.A.R. Hoare

In this edition of the Papers We Love series, Jean Yang, PhD student at MIT, presents on An Axiomatic Basis for Computer Programming by C.A.R. Hoare.

It is difficult to test all possibilities in complex systems--and practically impossible in concurrent systems. For the critical systems in our lives, we should demand mathematical guarantees that the software behaves the way the programmer expected.

A single paper influenced much of the work towards providing mathematical guarantees. C.A.R. Hoare’s seminal 1969 paper “An Axiomatic Basis for Computer Programming” introduces a method of reasoning about program correctness now known as Hoare logic. In this paper, Hoare provides a technique that

  1. allows programmers to express program properties and

  2. allows these properties to be automatically checked.

These ideas have influenced decades of research in automated reasoning about software correctness.

In this talk, Jean describes the main ideas in Hoare logic, as well as the impact of these ideas. She also covers her personal experience using Hoare logic to verify memory guarantees in an operating system.


This talk was recorded at the Papers We Love meetup at Viggle.