University Homepage School Homepage School Contacts School Search

Automated Reasoning: Coursework Files

Coursework Assignment 1, 2012-2013: Theorem Proving in Isabelle

Update: The command for submitting your completed assignments has been updated to reflect the new version of 'submit'.

The following files are for the first Automated Reasoning coursework assignment.

Required Files for MSc:

• MSc Coursework Assignment Sheet 1.
• You must complete and submit the following theory file: msc.thy
• Submit your assignemnt by typing: submit ar 1 msc.thy

Required Files for UG4:

• UG4 Coursework Assignment Sheet 1
• You must complete and submit the following theory file: ug4.thy
• Submit your assignemnt by typing: submit ar 1 ug4.thy

Useful Material:

• Lecture Slides
• Isabelle Startup Guide
• Isabelle FAQ
• Isabelle Cheat Sheet

Your work should be submitted by 4pm on Friday 26th October 2012 .

Solutions:

• UG4 solutions 1
• MSc solutions 1
• Note that these are not intended to be an optimal set of solutions. There are many other solutions to these problems which will earn full marks.

The demonstrator, Yuhui Lin (Y.H.Lin-2@sms.ed.ac.uk), will be available to give advice on Isabelle on Wednesdays from 4pm-5pm in room AT 4.12 and on Thursdays from 2pm-3pm in room AT 4.12. You may also email the demonstrator about the first assignment outside these hours.

---

Coursework Assignment 2, 2012-13: Model-Checking with NUSMV

The first part of this assignment was issued on Thursday 8th November. The rest on Monday 12th November.

Your work should submitted by 12:00 on Monday 26th November 2012.

Required Files: (UG4 & MSc unless otherwise stated)

• Coursework Assignment Sheet 2
• ltl-exercise.smv
• ctl-exercise.smv
• bridge.smv
• bridge-properties.smv
• bridge-ltlmc.smv (MSc only)

Useful Material:

• Slides from NuSMV lecture
• NuSMV Startup Guide

Lab Sessions:

The demonstrator, Andrew Sogokon, will be available to give advice in room AT 4.12 at the times:

• Wed 14th Nov, 4-6pm,
• Thu 15th Nov, 2-3pm,
• Mon 19th Nov, 2-3pm,
• Wed 21th Nov, 4-6pm,
• Thu 22nd Nov, 2-3pm.

You can also ask questions on the course Discussion Forum, or email the demonstrator or 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.