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