Internal Project Pages

These are the internal project pages for the SPADEase project.

Hums

Hums are short notes written to document the progress of the SPADEase project. For the curious: 'Hum' refers to both the Praxis Humming bird and Winnie-the-Pooh's indirect approach to writing: "Poetry and Hums aren't things which you get, they're things which get you."

Hum 1 - Six Months

This note was written prior to arriving in Praxis. It describes a plan of work for the six month duration of the secondment.

Hum 2 - The SPADE Helper Architecture

Develops and describes the architecture for the central SPADEase component. (Note that SPADEase was originally called the SPADE Helper)

Hum 3 - Tweaking the SPADE Simplifier

Describes changes made to the SPADE Simplifier so that it has a new qualifier (/norenum) which when provided will prevent the SPADE Simplifier from renumbering the conclusions loaded from the VCG file in the SIV file. (This makes it straight forward to relate the SIV file to the VCG file)

Hum 4 - Tweaking the SPADE Proof Checker

Describes various changes made to the SPADE Proof Checker so that it supports a new mode: 'tame'. While operating in this mode the SPADE Proof Checker operates in a more constrained manner, making it easier to control via external tools. Note that these changes are presented as a first draft - to be tweaked as the SPADEase tools progress.

Hum 5 - iSpeak @ 1st SE Co-Ex @ Px-HIS

I was invited to give a presentation at the first meeting of the Software Engineering Community of Expertise within Praxis High Integrity Systems (SE Co-Ex @ Px-HIS). This note collects the slides, bullet point notes, and question and answers associated with this presentation.

Hum 6 - Porting the SPADE Proof Checker to SICStus (Reissue)

A slightly modified version of a note written during the NuSPADE project, documenting the changes made to the SPADE Proof Checker (and the problems encountered) in porting it to SICStus.

Hum 7 - Hey, what does the SPADEase-Parser look like, anyway?

The SPADEase-Parser is an unforeseen component in the (early) original design of SPADEase. This note clarifies the behaviour of the SPADEase-Parser and outlines some high level implementation details.

Hum 8 - A little story of a large bug

This was written to document a bug that caused much aggro in the development of the SPADEase-Parser. The note serves little purpose beyond a gentle reminder of the perils of programming and the problems that might be encountered if modifying the core NuSPADE system.

Hum 9 - And the SPADEase-Planner

This continues the high level design approach seen in Hum-7, this time for the SPADEase-Planner.

Hum 10 - SPADEase: The Good, the Bad and the Ugly

Andrew Ireland visited Praxis to catch up on the progress of SPADEase. Part of this visit included a lunchtime seminar describing the status of SPADEase. This note collects the slides and a scattering of notes associated with this presentation.

Hum 11 - Adventures with PolySpace and friends

As an aside to the core SPADEase project, some analysis and research was conducted about the performance of program analysis systems. Particular emphasis was placed on exploiting our current full version (academic licence) of PolySpace.

Hum 12 - Revisiting the SPADE Proof Checker

Here the changes made to the Proof Checker are revisited, in reaction to the problems experienced in Hum-4. The selected solution is introducing a single, powerful, command to the Proof Checker. Unfortunately, this command circumvents the existing Proof Checker code and thus raises genuine soundness concerns. While it is accepted that the solution is not ideal, it appears the best option in the time available.

Hum 13 - Let there be PropGen-Light

The SPADEase project has focused on proof planning over program analysis. However, if finding time, some limited program analysis within SPADEase could be pursued. Here changes to create a light version of NuSPADE's program analysis program PropGen are considered.

Hum 14 - Improved Term Simplification

Term simplification employed in NuSPADE does not apply in SPADEase. This note documents the problems encountered, and how they were overcome. In particular, it describes a move away from a centralised simplification strategy and the introduction of a new, annotation based, term attraction simplification heuristic.

Hum 15 - No one said it'd be easy: SPADEase Version 1

This note marks the completion of the first version of SPADEase, illustrated with a single example. Brief remarks are about the success of the SPADEase project given the production of this system.

Hum 16 - SPADEase experiment

The SPADEase system is applied to the remaining, provable, problems seen when verifying the SHOLIS system. Comments are made about how the experiment was conducted and conclusions are drawn about the value of SPADEase.

Reports

This contains the final reports. These are also publicly available.

Presentations

This collects the PowerPoint files from SPADEase related presentations. These presentations are also publicly available.