Logics of Programs

Workshop, Yorktown Heights, NY, USA

herausgegeben von D. Kozen

Proof rules dealing with fairness.
Hoare's Logic is incomplete when it does not have to be.
The refinement of specifications and the stability of Hoare's Logic.
Toward a logical theory of program data.
Design and synthesis of synchronization skeletons using branching time temporal logic.
The type theory of PL/CV3.
Correctness of programs with function procedures.
A formalism for reasoning about fair termination.
Keeping a foot on the ground.
Further results on propositional dynamic logic of nonregular programs.
Some observations on compositional semantics.
Some connections between iterative programs, recursive programs, and first-order logic.
On induction vs. *-continuity.
Timesets.
Program logics and program verification.
Verification of concurrent programs: Temporal proof principles.
Synthesis of communicating processes from Temporal Logic specifications.
A note on equivalences among logics of programs.
The representation theorem for algorithmic algebras.
Nonstandard Dynamic Logic.
A critique of the foundations of Hoare-style programming logics.
Some applications of topology to program semantics.
Using graphs to understand PDL.
Critical remarks on max model of concurrency.
Transcript of panel discussion.