Announcements:

Oct. 18: A new project distribution is available. The old one has DOS CRLF in it.

Oct. 12: Homework due in class on Oct. 19th

·        Consider a theory with the axioms \forall p.pAB = pB and \forall p.pBC = pD. I write tA for the application of the unary function A to the term t. Derive a closure operation for this theory, following the model used in lecture. Prove that the extension of congruence closure with this operation is complete. Hint: the conjunction of literals xA=yA and xD <> yD is not satisfiable, and your algorithm should discover that.

·        Give an example of a theory consisting only of unary functions and equality axioms as above (with only only quantified variable) for which the procedure discussed in class for deriving a closure operation (based on constructing rules that add nodes to the EDAG), obtains a closure operation that is not guaranteed to terminate.

Sep 28: The project instructions are online.

Sep 24: Homework due in class on Oct 5th

·        Give another example on a non-convex theory (other than sel/upd and integer arithmetic)

·        Show that if all the axioms of the theory are of the form \forall x.f1(f2(…(fn(x))) = g1(g2(…(gm(x))), along with the usual equality and congruence axioms, then the theory is convex. The unary function symbols may appear several times in an axiom like the above.

·        Is this still true if we also allow disequalities in the axioms?

Sep 9: Homework due in class on Sep 13th

·        Prove the soundness and completeness of VCGen (statements on slide 64 of lecture notes for lecture 2). A sketch of the proof is enough, with a statement of the precise statement to be proved. Focus on loops.

Sep. 3: I need volunteers for the following lectures:

·        JML specification language and ESC-java. I envision this as a half-lecture, half-demo of ESC Java