## The electronic documets: day 3

Well, I got through 20 articles today. Today's batch includes:

- Two non-technical articles I apparently found on the web. One compared FM with XP, while the other just had some useful references to programming languages with a formal semantics.
- Both volumes of
*An Internationsl Survey of Industrial Applications of Formal Methods*. This one is a collection of 12 case studies in real formal methods use. - Two items on ROOL, the Refinement Object-Oriented Language, by Cavalcanti and Naumann. One is actually just some lecture slides, but the other is a
*wp()*semantics of the language. - An extensive guide to formal methods that was written to supplement the FAA's Digital Systems Validation Handbook. I don't know
*where*I found that. - Two papers on Z. One answers a challenge to examine the questions raised in converting an English specification (of an invoicing system) into a formal one, while the other compares Z to VDM and some other formal methods.
- A truly baffling article by Naumann called
*A Categorical Model for Higher Order Imperative Programming*. I'm still not sure exactly what it's about, but it appears to involve set theory. At least, that's what I got from skimming the introdiction. The abstract might as well have been gibberish for all the good it did me. - An interesting sounding paper that used case studies to examine why formal methods are not more widely used.
- A doctoral thesis of a formal verification of thttpd, a secure web server.
- An article on formal reasoning about pointers using Higher Order Logic. (Used Isabelle/HOL for automated proofs.)
- A case study on using "lightweight" formal methods to analyze and detect problems with the design of a radiation therapy machine.
- A paper that gives a sound and complete Hoare logic for a language with recursion and unbounded nondeterminism. (This one also uses Isabelle/HOL. I guess I should look into that.)
- An intriguing critique of Hoare logics in general. Apparently, Hoare logics are generally not "inferentially sound," but rather "theorem sound," which the author finds unacceptable. Apparently, this is related to the difference between partial and total correctness. The author also bangs on about
**goto**statements. This one sounds very interesting. - An apparently reworked version of Nelson and Broy's article on adding fair-choice to Dijkstra's calculus. It looked an awful lot like the one from yesterday, but the publication date was four years later. Maybe the ACM just published an edited version.
- A "practical guide" to defining programming languages using Prolog and Metamorphosis Grammars, which includes relational, denotational, and axiomatic semantics.
- An article describing a verification tool that works by verifying abstract programs and relating them to concrete programs.
- Last, but not least, an account of the Stanford Pascal verifier.

Looks like I'm nearly done. I've got about 15 documents left. Most of them are on SPARK and written by good people at Praxis Critical Systems.

You can reply to this entry by leaving a comment below. This entry accepts Pingbacks from other blogs.

## Add your comments #

A comment body is required. No HTML code allowed. URLs starting with http:// or ftp:// will be automatically converted to hyperlinks.