CS 477: Formal Software Development Methods main  ::  policy  ::  lectures  ::  mps  ::  exams  ::  unit project  ::  resources  ::  faq
Machine Problems for Spring 2018
Topic: Issued: Due at 9:00pm CT on: Automatic extension(with 20% penalty)until 9:00pm Solution File CT on: Propositional Logic in Isabelle, mp1.thy Wednessday, Feb 7 Wednesday, Feb 14 Friday, Feb 16 mp1_sol.thy Verifying Basic Operations on Boolean Expressions (mp2.thy) Wednesday, Feb 14 Wednesday, Feb 21 Friday, Feb 23 mp2_sol.thy Hoare Logic Proofs in Isabelle/HOL Thursday, Mar 15 Wednesday, Mar 28 Friday, Mar 30 mp3_sol.thy Evaluation Semantics Friday, Mar 30 Friday, Apr 6 Sunday, Apr 8 mp4_sol.thy Program Transition Systems and Linear Temporal Logic Friday, Apr 10 Friday, Apr 17 Sunday, Apr 19 mp5_sol.thy Modeling in Promela and SPIN Monday, Apr 23 Wednesday, May 2 Friday, May 4 mp6_sol.tgz

Hand Written Assignments for Spring 2018
Topic: Issued: Due at 9:00pm CT on: Automatic extension(with 20% penalty)until 9:00pm Solution Files CT on: Truth and Proof in Propositional Logic, revised hw1.tex mphandout.cls macros.tex prooftree-doc.pdf prooftree.sty prooftree.tex sample_proof_tree.tex sample_proof_tree.pdf Wednesday, Jan 24 Wednesday, Jab 31 Friday, Feb 2 hw1-sol.pdf Binary Decision Diagrams Wednesday, Jan 31 Wednesday, Feb 7 Friday, Feb 9 hw2-sol.pdf Interpretation and Proof of First Order Logic Formulae Wednesday, Feb 21 Wednesday, Feb 28 Friday, Mar 2 solution pdf:hw3-sol.pdf thy:hw3_sol.thy

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 svn co https://subversion.ews.illinois.edu/svn/sp18-cs477/
• 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 ""
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 9:00pm on the due date is that one that will be collected and graded.