System Modelling and Design, Extended Stream: Proofs
COMP2111 XT is an extended stream of lectures for COMP2111. COMP2111 is about system modelling and design, about how to build software that works. The lecture shows engineering methods, many based on formulas and proofs, demonstrated in the B method. The extended stream for this lecture offers a broader view of what other tools and methods exist, and shows some cool projects that use(d) formal modelling and proofs.
The extended stream is one additional hour of lecture per week. It is completely voluntary, fun, and interest based. There is no home work, no assessment, and no additional credit. There are no prerequisites either, the extended lectures are open to all.
The extended lectures are taught by June Andronick (UNSW Conj Lecturer, NICTA Researcher) and Gerwin Klein (UNSW Sen Con Lecturer, NICTA Principal Researcher) from NICTA's Formal Methods and ERTOS groups.
Topics include:
- How do I build software that actually works? (Techniques overview and cool projects that did it)
- What's in a proof? (Natural Deduction)
- The proposition. (Propositional logic tools)
- Vampires and other demons of the 1st order. (First order logic and automation)
- Hey, check out this model! (SPIN and model checking)
- A functional program? (Equations and recursion)
- A symbolic execution. (Proof by term rewriting)
- Induction, supernatural. (Proof by structural induction)
- States and imperatives. (Pre- and post conditions, Hoare logic)
- Terminate. Will it? (Proof of program termination)
Session times:
- Thu, 11:00h - 12:00h (L5, NICTA, Level 1 Seminar Room)