I've gotten through the remainder of my paper articles. I still have to go over my accumulated notes, but most of them are on the articles I've been cataloging here.
I had 10 articles today. They include:
- An article describing a wp() refinement calculus. It seems to focus on a "refinement relation" for preserving total correctness between steps in program derivation.
- An article on integrating FM into development. It describes the Secure Release Terminal (a system for changing classified document security) and the use of the the Ina Jo specification language.
- An interesting article on teaching FM in a "general education" computer science course.
- A paper describing KIDS, an interactive system for automatically developing programs. The idea is that all the hard work is automated and you can build a formal specification just by selecting various high-level transformations. It gives a derivation of a program to solve the k-queens problem as an example.
- An interesting looking article on reasoning about the effects of program changes. It uses an approximate logic and works on the structure, rather than semantics, of the program.
- Greg Nelson's generalization of Dijkstra's calculus. Essentially, he removed the Law of the Excluded Miracle, i.e. wp(S, false)=false. This gives us the possibility for partial commands and other things I don't want to think about at 10:30 at night.
- A round-table series of articles on formal methods. It's just a series of one-page articles on FM topics ranging from education to industrial use.
- An article on the Penelope "verification editor" for Larch/Ada. Apparently it's another interactive tool, but this one uses the Larch Shared Language to generate verification conditions for a subset of Ada.
- A paper on "debugging" Larch specifications. It describes a couple of tools that check various claims that can be included in Larch specifications.
- An article on using the Boyer-Moore prover to automatically verify concurrent programs. Describes the logic and semantics used and gives the example of a distributed program to compute a minimum value in a tree.
I guess tomorrow I'll pick up on finishing off my mind-map and start thinking about a topic summary. That should be interesting, as staying on topic was where I had my problems the first time.