## Assignment 1

You may collect your marked assignment. Run (on a CSE machine):

`~cs4161/bin/classrun -collect a1`

or use the web interface.

Model assignment solution: [thy]

This UNSW course is about
mechanical proof assistants, how they work, and what they can be used
for. It is taught by members of the
Trustworthy Systems
group from Proofcraft and UNSW.
The course presents specification and proof techniques used in
industrial grade interactive theorem provers, teaches the theoretical background
to the techniques involved, and shows how to use a theorem prover to
conduct formal proofs in practice.

Topics include higher order logic, natural deduction, lambda calculus,
term rewriting, data types and recursive functions, induction
principles, and proofs about
programs. See the course outline for a full
content overview and prerequisites.

The course will provide hands-on experience with the proof assistant Isabelle/HOL.

Slides and Isabelle files will be made available online as the lectures progress.

Setting up Isabelle, basic rules and cheat sheet.

Textbook, further reading, and links the tools used in the lecture.

slides [pdf], slides with animations [pdf], intro demo [thy], lambda calculus demo [thy]

slides [pdf], slides with animations [pdf], demo [thy] demo solution [thy]

slides [pdf], slides with animations [pdf], demo [thy], demo solution [thy], Isar demo [thy]

slides [pdf], slides with animations [pdf], HOL demo [thy] automation demo [thy] exercise template [thy]

slides [pdf], slides with animations [pdf], introductory demo [thy] simp demo [thy]

slides [pdf], slides with animations [pdf], demo [thy], demo solutions [thy]

slides [pdf], slides with animations [pdf], demo [thy], solution [thy]

slides [pdf], slides with animations [pdf], demo [thy] solution [thy]

demo [thy] (as developed in the lecture)

slides [pdf], slides with animations [pdf], demo [thy], Isar demo [thy]

slides [pdf], slides with animations [pdf], demo [thy], demo solutions[thy]

slides [pdf], slides with animations [pdf], demo [thy], demo solutions[thy]

slides [pdf],
slides with animations [pdf],
demo [thy],
C file [c],

C-Parser and AutoCorres [tar.gz]

slides [pdf],
slides with animations [pdf],
**2014 exam papers:**
exam [pdf],
C file [c],
Isabelle template [thy].

**2014 exam solution:**
[pdf, thy].

**invariant practice** demo [thy]
and solutions [thy].

You may collect your marked assignment. Run (on a CSE machine):

`~cs4161/bin/classrun -collect a1`

or use the web interface.

Model assignment solution: [thy]

You may collect your marked assignment. Run (on a CSE machine):

`~cs4161/bin/classrun -collect a2`

or use the web interface.

Model assignment solution: [thy]

The exam will be a 24h take-home exam. It will start Mon, 29 Nov 2021, 8am AEDT (Sydney time), and end Tue, 3 Dec 2021, 7:59am AEDT (Sydney time).

You should use Isabelle 2021 and AutoCorres-1.8 for the exam (same as for assignment 3).

You may collect your marked exam. Run (on a CSE machine):

`~cs4161/bin/classrun -collect exam`

or use the web interface.

We are using Piazza for class discussions. Please post questions about lecture material or the assignments and so forth.

Consults by appointment.