Course

Advanced Topics in Software Verification - COMP4161

Faculty: Faculty of Engineering

School: School of Computer Science and Engineering

Course Outline: www.cse.unsw.edu.au/~cs4161

Campus: Sydney

Career: Postgraduate

Units of Credit: 6

EFTSL: 0.12500 (more info)

Indicative Contact Hours per Week: 3

Enrolment Requirements:

Prerequisite: Completion of 48 UOC

CSS Contribution Charge: 2 (more info)

Tuition Fee: See Tuition Fee Schedule

Further Information: See Class Timetable

View course information for previous years.

Description

This course is about mechanical proof assistants, how they work, and what they can be used for. It presents specification and proof techniques used in industrial grade theorem provers, teaches the theoretical background to the techniques involved, and shows how to use a theorem prover to conduct formal proofs in practice. The courses is intended to bring third/fourth year and postgraduate students into contact with the current research topics in the field of theorem proving and automated deduction and to teach them the necessary skills to successfully use industrial grade verification environments in modelling and verification.

Topics covered included: higher order logic, natural deduction, lambda calculus, term rewriting, data types and recursive functions, induction principles, calculational reasoning, mathematical proofs, decision procedures for a variety of logical domains, and proofs about programs.

Note: experience with (first-order) logic and functional programming is required.
Computing Logo

Study Levels

UNSW Quick Links