CS 477: Formal Software Development Methods
Machine Problems for Spring 2013
Topic: Issued: Due at 11:59pm CT on: Automatic extension
(with 20% penalty)
until 11:59pm CT on:
Solution File
MP1 Propositional Logic in Isabelle Thursday, Jan 31 Friday, Feb 8 Sunday, Feb 10 mp1-sol.thy
MP2 Hoare Logic Proofs in Isabelle/HOL Sunday, Feb 24 Sunday, Mar 3 Tuesday, Mar 5 mp2-sol.thy
MP3 Modeling Friday, Apr 12 Friday, Apr 19 Sunday, Apr 20
MP4
MP5

Hand Written Assignments for Spring 2013
Topic: Issued: Due at 11:59pm CT on: Automatic extension
(with 20% penalty)
until 11:59pm CT on:
Solution Files
HW1 Truth and Proof in Propositional Logic Wednesday, Jan 23 Wednesday, Jan 30 Friday, Feb 1 hw1-sol.pdf
HW2 Interpretation of First Order Logic Formulae Friday, Feb 8 Friday, Feb 15 Sunday, Feb 17 hw2-sol.pdf
HW3 Floyd-Hoare Logic Saturday, Feb 16 Friday, Feb 22 Sunday, Feb 24 hw3-sol.pdf
HW4 Evalation Semantics Sunday, Mar 31 Sunday, Apr 7 Thursday, Apr 9 hw4-sol.pdf
HW5

Note: The late penaly is 20% of the total number of points possible on the base part of the assignment, plus 20% of the total points possible on the extra credit, if you attempt the extra credit. It is not 20% of the number of points your earn.

Instructions for Submitting Assignments
  • Each student is given an svn directory that needs to be checked out at the beginning of the semester to as follows:
    mkdir <working_directory>
    svn co https://subversion.ews.illinois.edu/svn/sp13-cs477/<your_netid> <working_directory>
  • After the initial checkout, <working_directory> will contain a subdirectory assignments. Once an assignment (mp or hw) has been announced, if you do an
    svn up
    you will add a directory named after the assignment (e.g. mp1) in the mps directory. That directory will contain instructions for the assignment, plus a stub for each file you must turn in.
  • To do an assignment, you will need to follow the instructions given in the directory for that assignment. There will be two kinds of assignments, mps and hws. Mps will be exercises carried out on tools supporting a specific type of formal methods. Hws will be written assignments proving theorems and doing hand calculations. Since the mps involve using various tools, by default you will need to do them on the ews linux machines. Most of the tools should also be avialable form the web to download to you own machine should you choose to work on your own machine.
  • To submit an assignment, once you have completed the necessry files as decribed in the assignment instructions, in the assignment directory or either of the parent directory or the gradparent directory
    svn commit -m "<your comment here>"
    You may restrict svn commit to a specific collection of files and directories by adding a list to the end of the command.
  • You may do multiple commits; the version that is in the repositry at 11:59pm on the due date is that one that will be collected and graded.