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

**Oct. 12: ****Homework due in class on**** Oct. 19 ^{th} **

·
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 5 ^{th}**

·
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 13 ^{th}**

·
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