goto UNSW  home page  
Contacts Library myUNSW WebCT
 Advanced Topics in Software Verification - COMP4161
PRINT THIS PAGE
 COMP4161
   
   
   
 
Campus: Kensington Campus
 
 
Career: Undergraduate
 
 
Units of Credit: 6
 
 
EFTSL: 0.125 (more info)
 
 
Contact Hours per Week: 4
 
 
Fee Band: 2 (more info)
 
 
Further Information: See Class Timetable
 
  

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 teh current research topics in the field of theorem proving and automated deduction and to teach them the necessary skills to sucessfully 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.

Further Information

URL for this page:

© The University of New South Wales (CRICOS Provider No.: 00098G), 2004-2011. The information contained in this Handbook is indicative only. While every effort is made to keep this information up-to-date, the University reserves the right to discontinue or vary arrangements, programs and courses at any time without notice and at its discretion. While the University will try to avoid or minimise any inconvenience, changes may also be made to programs, courses and staff after enrolment. The University may also set limits on the number of students in a course.