| Machine Problems for Spring 2018 |
|
Topic: |
Issued: |
Due at 9:00pm CT on: |
Automatic extension
(with 20% penalty)
until 9:00pm
CT on: |
Solution File |
| MP1 |
Propositional Logic in Isabelle,
mp1.thy |
Wednessday, Feb 7 |
Wednesday, Feb 14 |
Friday, Feb 16 |
mp1_sol.thy |
| MP2 |
Verifying Basic Operations on Boolean Expressions
(mp2.thy) |
Wednesday, Feb 14 |
Wednesday, Feb 21 |
Friday, Feb 23 |
mp2_sol.thy |
| MP3 |
Hoare Logic Proofs in
Isabelle/HOL |
Thursday, Mar 15 |
Wednesday, Mar 28 |
Friday, Mar 30 |
mp3_sol.thy |
| MP4 |
Evaluation Semantics |
Friday, Mar 30 |
Friday, Apr 6 |
Sunday, Apr 8 |
mp4_sol.thy |
| MP5 |
Program Transition Systems and Linear Temporal Logic |
Friday, Apr 10 |
Friday, Apr 17 |
Sunday, Apr 19 |
mp5_sol.thy |
| MP6 |
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
CT on: |
Solution Files |
| HW1 |
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 |
| HW2 |
Binary Decision Diagrams
|
Wednesday, Jan 31 |
Wednesday, Feb 7 |
Friday, Feb 9 |
hw2-sol.pdf |
| HW3 |
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 |
| HW4 |
| | | | |
| HW5 |
| | | | |
| HW6 |
| | | | |
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/sp18-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
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 9:00pm on the due date is that one that
will be collected and graded.
|