The Model Checker Blast: Applications to Software Engineering

Download paper.
Go to Blast home page for tool download.

Figures in vector graphics format

Some of the figures for the running example in Section Software Model Checking might not be perfectly readable in a printout. Therefore we provide SVG versions of the figures here, which also support zooming.

Figure	File
Fig. 1: The example C program	example.c
Fig. 2: Control-flow automaton for function main	fig-example-cfa-main.svg
Fig. 3: Control flow automaton for function altInit	fig-example-cfa-altInit.svg
Fig. 4: Complete abstract reachability tree	fig-example-rt4.svg
Fig. 5: Abstract reachability tree when the first infeasible error path is found	fig-example-rt1.svg
Fig. 8: Abstract reachability tree when the second infeasible error path is found	fig-example-rt2.svg
Fig. 7: Abstract reachability tree when the third infeasible error path is found	fig-example-rt3.svg

Example programs for checking memory safety

The original programs are taken from the following sources:
from the Olden v1.0 benchmark suite (zip archive, browse directory): bisort, em3d, power, treeadd, tsp, perimeter, mst
from the C SPEC95 benchmark suite (zip archive, browse directory): li
the scheduler for Unix systems fcron (zip archive, browse directory): fcron
All sources together in one archive (zip).

Program	Original source code	Cured source code	Opimized source code
Bitonic Sort algorithm	bisort	bisort.cured.c	bisort.optimized.c
Electromagnetic Problem in Three Dimensions	em3d	em3d.cured.c	em3d.optimized.c
Power Pricing problem	power	power.cured.c	power.optimized.c
Tree Add example	treeadd	treeadd.cured.c	treeadd.optimized.c
Traveling Salesman problem	tsp	tsp.cured.c	tsp.optimized.c
Perimeters algorithm	perimeter	perimeter.cured.c	perimeter.optimized.c
Minimum Spanning Tree problem	mst	mst.cured.c	mst.optimized.c

scheduler for Unix systems fcron, version 2.9.5	fcron-2.9.5	fcron.cured.c	fcron.optimcured.c
Lisp interpreter	130.li	li.cured.c	li.optimcured.c

Example programs for test-case generation

The first five programs are Windows NT device drivers,
ping is the network sevice client for the ping protocol,
ftpd is an server program for the FTP protocol.
All sources together (zip archive, browse directory).

Program	Preprocessed source code
kbfiltr	kbfiltr.i
floppy	floppy.i
cdaudio	cdaudio.i
parport	parport.i
parclass	parclass.i

ping	n.a.
ftpd	n.a.