Flexible proof reuse for software verification

Proof reuse, or analogical reasoning, involves reusing the proof of a source theorem in the proof of a target conjecture. We have developed a method for proof reuse that is based on the generalisation replay paradigm described in the literature, in which a generalisation of the source proof is replayed to construct the target proof. In this paper, we describe the novel aspects of our method, which include a technique for producing more accurate source proof generalisations (using knowledge of the target goal), as well as a flexible replay strategy that allows the user to set various parameters to control the size and the shape of the search space. Finally, we report on the results of applying this method to a case study from the realm of software verification.

Computer animation of hot spot development in bulk coal as an aid for training coal miners

The processes that take place during the development of a heating are difficult to visualise. Bulk coal self-heating tests at The University of Queensland (UQ) using a two-metre column are providing graphic evidence of the stages that occur during a heating. Data obtained from these tests, both temperature and corresponding off-gas evolution can be transformed into what is effectively a video-replay of the heating event. This is achieved by loading both sets of data into a newly developed animation package called Hotspot. The resulting animation is ideal for spontaneous combustion training purposes as the viewer can readily identify the different hot spot stages and corresponding off-gas signatures. Colour coding of the coal temperature, as the hot spot forms, highlights its location in the coal pile and shows its ability to migrate upwind. An added benefit of the package is that once a mine has been tested in the UQ two-metre column, there is a permanent record of that particular coals performance for mine personnel to view.