CS3001 Formal Methods

This page will provide materials to support the JS option in formal methods, listing lecture notes, exercises and useful links.

Official CS3001 Page

CS3001 Timetable

Classes

• Week 1 : Class 1 | Class 2 | Class 3
  - Floyd 1967 paper | Hoare 1969 paper
• Week 2 : Class 1 | Class 2 | Class 3
• Week 3 : Class 1 | Class 2 | Class 3
• Week 4 : Class 1
• Week 5 : Class 1 | Class 2 | Class 3
• Week 6 : Class 1 | Class 2 | Class 3
• Week 7 : reading week
• Week 8 : Class 1 | Class 2 | Class 3
• Week 9 : Class 1 (St. Patrick's Day)
• Week 10 : Class 1 | Class 2 | Class 3
• Week 11 : Class 1 | Class 2 | Class 3
• Week 12 : Class 1 | Class 2 | Class 3

Coursework (20%)

Project (10%)

Mini-Exercises (10%)

Now available in the above document (unless linked otherwise):

• Mini 1 Exercise | Solutions
• Mini 2 Exercise | Solutions
• Mini 3 Exercise | Solutions
• Mini 4 Exercise | Solutions
• Mini 5 Exercise | Solutions
• Mini 6 Exercise | Solution to Proofs 1-4

Examination (80%)

Sample Exam Paper (2009)
Annual Exam Paper (2009)

Software

Readings/Links

• CS3001 Reference (Useful Definitions and Laws)
• Draft User Manual for Saoithín (version: 15/3/2010)
• Original Mondex proof publication
• Handbook of Mathematics for CS (2005)
• Formal Methods Virtual Library
• Formal Methods (Wikipedia)
• Formal Methods Europe
• Laws of Programming
• How not to prove something (anything !)

FAQ

• What is the weighting between coursework and exam?

  Exam: 80%, Project: 10%, MiniExercises: 10%

• I was just wondering if the questions in the exam paper will have clear sections like the sample paper or a more integrated approach in regards to the sections?

  They will have clear sections just like the sample paper.
  The precise number of sections in each question may differ from that in the sample paper.
  The marks awarded per section may differ from those in the sample paper.