Spurinna

Disclaimer: This software was developed as a research prototype. Its operation has not been formally (or informally...) verified. Its use in safety or security critical applications is not supported. The system specifications available here have not been verified and are intended as examples and suggestions only.

JAR archives

These can be executed with the command "java -jar Spurinna.jar"

Latest: Spurinna.jar

System specifications

If you identify any faults in these specifications, or if you would like to submit additions to this collection, please contact Ramsay Taylor.

IA-32 (i386)

This is the (very) partial spec used in the thesis examples.

AVR (ATTiny)

This is a partial spec of the AVR instruction set, specifically the ATTiny instruction set. Although, its only part of that...

Examples

The example disassembly files used in the thesis are available here:

References

The operation of the analysis process, and several small examples of analysis and verification are included in my PhD thesis.

This paper from ABZ2012 is a more concise introduction but does not contain the detailed examples or the technical detail.

All software on this page is distributed under the terms of GPL3