
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 


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
prooftreedoc.pdf
prooftree.sty
prooftree.tex
sample_proof_tree.tex
sample_proof_tree.pdf
 Wednesday, Jan 24 
Wednesday, Jab 31 
Friday, Feb 2 
hw1sol.pdf 
HW2 
Binary Decision Diagrams

Wednesday, Jan 31 
Wednesday, Feb 7 
Friday, Feb 9 
hw2sol.pdf 
HW3 
Interpretation and Proof of First Order Logic Formulae 
Wednesday, Feb 21 
Wednesday, Feb 28 
Friday, Mar 2 
solution pdf:hw3sol.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.
