History for Outline of Theory Challenges

changed:
-  * concurrency (TODO O'Hearn)
-
-    There are numerous abstract models of concurrency suitable for requirements and specification and design refinement.
-For verification of code, however, we need good semantics for shared-memory concurrency with weakly consistent memory models. Lock-free programs and transactional memory appear promising and important but extant work is relatively informal.
-Theories like separation logic (Reynolds, O'Hearn, et al) and Boogie (Leino et al) have good modularity properties but are only at the level of source code.  A gap remains between designs and concrete code.  Specification-oriented semantics, e.g., Reynolds' grainless concurrency model may help here.
  * concurrency [[Concurrency]]