Crowfoot Tool | Project | Informatics


Help pages regarding our verifier for programs using stored procedures

Sponsored by Project From Reasoning Principles for Function Pointers To Logics for Self-Configuring Programs" (EP/G003173/1)
The University of Sussex
EPSRC Research Funding
[ updateable webserver example ]
This section details an example of using Crowfoot to verify runtime updates. Specifically, we give an implementation, in Crowfoot's input language, of the (idealised) updateable webserver from the paper "Formalizing Dynamic Software Updating" by Bierman, Hicks, Sewell and Stoyle. We present Crowfoot input files for three versions, or stages, of the example.
  1. Initial version: Here we implement and prove the updateable webserver. This proof would be done before we start the server running.

  2. Version with one update: Here we add to the code an update which adds logging, so that a record is kept of every event handled. This proof would be done when the server is already running, once we have decided on the need for, and programmed, the update.

  3. Version with two updates: This code includes the update to add logging, and then another, later update to change the type of events handled, using the "convert" strategy to deal with events already in the queue. This proof would be done when the server is running with the first update (to add logging) already in place, once we have programmed the second update.
The following images show examples of the graphical output which Crowfoot can generate to explain its proofs. They are taken from the proofs of the version with one update.
  1. Graph 1: This shows the symbolic execution of the 'update' procedure. One can see some ghost statements that perform folding and unfolding of predicates, and one can see the nested triples appearing in assertions as procedures are written to the heap.

  2. Graph 2: This shows the symbolic execution of the 'handle' procedure. One sees the branching of the symbolic execution tree, produced by, among other things, if-then-else statements. Yellow nodes are where the symbolic state was found to be inconsistent (and thus there was no further work to do). Green nodes show where the end of the procedure body was reached, and an appropriate postcondition was proved to hold.

  3. Graph 3: This shows a proof of an entailment between assertions, which arises while checking the 'handle' procedure; this proof obligation corresponds to the rightmost green box in Graph 2.

Page maintained by Crowfoot Team