COMP60332: Automated Reasoning and Verification (2020-2021)

Delivery is from the start od Semester 2 (second week of February 2021) for 6 weeks.

Course description

Follow this link for the course unit description, giving details about the aims and learning outcomes of the course, reading material, assessment, and the syllabus.

• Link to ACS Syllabus

Locations and times

Teaching team

Lecturers

• Konstantin Korovin
• Renate Schmidt

Teaching assistants

Coursework

Handing in your work: Please submit your scanned in written coursework as a pdf file to Blackboard.

Slides, videos and notes

• Introduction to the Theme: Software Security and Automated Reasoning Theme intro talk
• Please refer to Blackboard for the weekly material and tasks

Other resources

• SMT solver (to be provided)
• MiniSAT Website
• DIMACS -- format for propositional satisfiability
• SPASS Website
• SPASS Tutorial

Pre-requisites

We will be assuming familiarity with the basic notions of sets, relations and functions. This will not be covered in lectures, but will be part of the first coursework sheet.

If you feel you want to review these notions we suggest you refer to one of:

• The chapter entitled "Sets etc" in Cormen, T. H. and Leiserson, C. E. and Rivest, R. L. (1992), Introduction to Algorithms. The MIT Electrical Engineering and Computer Science Series, MIT Press. In some editions it is in Chapter 5.2, and in others it is in the Appendix.
• Chapters 1.1, 1.2 and 1.3 of "Interactive Real Analysis". This website includes interactive exercises with answers.
• Any book on the mathematical foundations of CS or discrete mathematics.

Knowledge of propositional logic and first-order logic would be some advantage, but is not essential as the course will introduce these.

Reading material

The course does not follow a specific book: copies of the slides are made available.

Recommended reading material is listed in the course unit description in the ACS Syllabus. Further references may be given during lectures.

There is no need to buy a book. All books are available in the Resources Centre Library (ask in SSO) or the main library.

Assessments

50% coursework, 50% exam

Past exam papers: It may be useful to refer to past exam papers also of COMP61111 and COMP60121 of previous years.