Automated Reasoning: Coursework Files

Coursework Assignment 1, 2013-2014: Software verification using Hoare logic in Isabelle

For this assignment you are required to generate proofs for some theorems in Isabelle. It is divided into two sections:

Required Files:

Submit your assignment by typing:

Useful Material:

Your work should be submitted by 2pm on Monday 28th October 2013 .

The demonstrator, Petros Papapanagiotou, will be available to give advice on Isabelle in the West Lab (5.05) of Appleton Tower each Thursday between 2pm and 3pm.
You may also email the demonstrator about the first assignment outside these hours.

Discussion Forum

Coursework Assignment 2, 2013-14: Model checking with NuSMV

To prepare for the assignment, consult the course's NuSMV Startup Guide

Required Files:

Useful Material:

Lab Sessions:

Lab sessions in Appleton Tower 5th floor Computer Lab North (5.04) or Computer Lab South (5.08), as indicated below. At each session, at least one demonstrator will be on duty.

You can also ask questions on the course Discussion Forum, or email the lecturer Paul Jackson.

Submission Deadlines

Please note that extensions to coursework deadlines cannot be granted by the course lecturers. All requests for extensions should be directed to the ITO via the appropriate support form. These will then be logged and passed on to the appropriate Course Organiser for a decision.

Home : Teaching : Courses : Ar 

Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail:
Please contact our webadmin with any comments or corrections. Logging and Cookies
Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh