The Software 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.