History for Imperative Program Logics

changed:
-  We use "logic" in a broad sense, to include semantics, proof systems, perhaps even methodologies.  Many tools embody axiomatic semantics, which interpret to include proof systems, weakest precondition calculus and verification conditions, refinement calculus, or similar formal systems for correctness of programs with respect to pre-post specifications, intermediate assertions, and relational formulae. On one hand, axiomatic semantics should be validated in terms of models faithful to actual implementation (compiler, runtime system, instruction set). On the other hand, it serves to embody general rules of reasoning in a form that facilitates specification and reasoning about particular systems. Axiomatic semantics can also serve as basis for notions of program equivalence and refinement since it abstracts from details that may not be considered observable.
  We use "logic" in a broad sense, to include semantics, proof systems (perhaps even methodologies, which are in a sense derived rules). Many tools embody axiomatic semantics, which interpret to include proof systems, weakest precondition calculus and verification conditions, refinement calculus, or similar formal systems for correctness of programs with respect to pre-post specifications, intermediate assertions, and relational formulae. On one hand, axiomatic semantics should be validated in terms of models faithful to actual implementation (compiler, runtime system, instruction set). On the other hand, it serves to embody general rules of reasoning in a form that facilitates specification and reasoning about particular systems. Axiomatic semantics can also serve as basis for notions of program equivalence and refinement since it abstracts from details that may not be considered observable.

changed:
-  * code pointers (Must first-order specifications be abandoned?  Can the problems with denotational semantics of stored procedures, vs procedures as arguments as in Algol, be dodged to get good proofsystems? 
-
-  * Modular specification and reasoning with frame conditions for mutable heap structure.  Can separation logic be extended to richer data model and language features? Can the various ownership systems be combined and generalized?
  * Code pointers. Must first-order specifications be abandoned?  Can the problems with denotational semantics of stored procedures, vs procedures as arguments as in Algol (work in the 70s by, e.g., Olderog, Halpern, Damm and Josko,...), be dodged to get good proofsystems?  Code pointers are being revisited in low level code (e.g., Appel, Shao, Thieleke)

  * Modular specification and reasoning with frame conditions for mutable heap structure.  Can separation logic be extended to richer data model and language features? Can the various ownership systems be combined and generalized?  (Leino; Mueller; Parkinson; Birkedal)

changed:
-and several groups have shown this can be achieved less frightfully than might be expected (see for example the "JBook":http://www.inf.ethz.ch/personal/staerk/jbook).
-
-  TODO links to Mobius project, Spec#, Tan and Appel, what? 
-
and several groups have shown this can be achieved less frightfully than might be expected (see for example the "JBook":http://www.inf.ethz.ch/personal/staerk/jbook;
other recent work on logics for verification of low level code: Tan and Appel; Mueller in the Mobius project; Benton; Spec#; others?