Ian Wehrman has sent the following abstract for 11/11/09: In this talk, I present a trace semantics based on graphs: nodes represent the events of a program's execution, and edges represent dependencies among the events. The style is reminiscent of partially ordered models, though we do not generally require properties like transitivity or acyclicity. Concurrency and sequentiality are defined using variations on separating conjunctions, which are instances of model theories of separation logic and bunched logic. The model has pleasant algebraic properties, which follow from surprisingly simple proofs. I present a number of theorems about the general model, including the soundness of the laws of Hoare logic and the Jones rely/guarantee calculus. No particular languages or applications are studied; this is left to future work.