Imperative program logics

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.

Sequential code in commonly used languages like C and Java involves language features and design idioms pose problems for specification and verification not fully solved to date:

• 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)
• Inheritance versus modularity. Frame conditions for extended state in subtypes. Dynamically bound method calls and behavioral subtyping for reasoning in terms of static types.
• inline assembler, which exposes aspects of machine semantics that in well designed programs are carefully isolated
• Reentrant callbacks. When do object invariants hold?
• address arithmetic, or alternatively the abstraction/security properties obtained by disallowing address arithmetic
• use of ``pure'' program expressions in specifications

The literature offers solutions to individual problems under simplifying assumptions.

Challenge: Integrate some solutions to produce a proofsystem or semantics adequate for verifying interesting challenge codes. Develop a semantic model and verify soundness of the proofsystem (meta-theory which merits machine checking, as the point is to include a number of complicated language features) Such an integration is being attempted in JML.

For some purposes it is important to verify bytecode or other unstructured code, and several groups have shown this can be achieved less frightfully than might be expected (see for example the JBook; other recent work on logics for verification of low level code: Tan and Appel; Mueller in the Mobius project; Benton; Spec#; others?