CS410/510 Theorem Proving and Program Verification
How can we use computers to help us construct formal proofs? This
question is one of the oldest in computing; thanks to improved tools
and more powerful processors, it has been enjoying renewed attention
in recent years. Today, theorem provers are being applied
successfully in many domains, ranging from pure mathematics to
verification of programs and hardware. This course will provide a
practical introduction to this interesting and increasingly relevant
area.
The main part of the course will be a hands-on introduction to
interactive theorem proving using the Coq proof assistant. A proof
assistant doesn't prove things itself; rather, it helps a human
construct a proof more easily and reliably. We will begin by learning
how to verify properties of simple functional programs, and then
progress to proofs about other formal systems, such as programming
language semantics or finite automata.
If time permits, we will also look at fully automated theorem provers,
which work without direct human guidance. Although fundamental
undecidability results tell us that such provers cannot work 100% of
the time, they are nonetheless often very useful in practice. We will
hope to cover SAT-solving and cooperating decision procedures, which
are the basis for many recent tools and applications.
Text:
There is no printed textbook, but in the first part of the course
we will be using an excellent on-line textbook by Benjamin Pierce,
called Software Foundations ( https://softwarefoundations.cis.upenn.edu/ ).
Prerequisites:
There are no formal course prerequisites, but prior exposure to basic
discrete mathematics and formal proof is essential. For example,
undergraduates should certainly have completed -- and enjoyed! --
CS250 and 251, and preferably CS311. Prior exposure to functional
programming (e.g. CS457/557) is also be useful, but not required.
Class meetings:
Class meetings will proceed in tutorial
style: I'll present some lecture material and show some examples; then
you'll try some exercises. For this style to work, everyone will need
access to a laptop computer (running Coq) during the class meeting.
Requirements:
There will be weekly homework exercises and a take-home midterm and
final, all based on the Coq proof assistant.