Benchmark Models

Benchmark Models

We provide benchmark suites in goto-binary format. All of these benchmarks were extracted using goto-cc. Currently the following model-checkers support loading these models:

We provide the following versions of models:
  • [SRC] sources (if modified)
  • [PLA] plain models
  • [INS] instrumented models (including system functions)
  • [ABS] abstraction-instrumented models (including abstractions of string functions)

BenchmarkNotes [SRC] [PLA] [INS] [ABS]
Powerstone
SNU Real-Time
SNU Real-Time (nondet)
NECLA Static Analysis Benchmarks
SSH Control Flow (ssh-magic)
 
Windows Device Drivers

The following table contains links to models of Windows device drivers. They are compiled from sources of the Windows DDK version 6001.18001 using goto-cc version 3.3. Note that these models do not contain assertions.

HarnessDownload
Notes
WDF (KMDF) Drivers
DRIVER_CREATE
FLAT_SIMPLE
PNP_DEFERRED_IO_REQUESTS
PNP_IO_REQUESTS
WDM Drivers
FLAT_HARNESS
FLAT_SIMPLE_HARNESS
FLAT_DISPATCH
FLAT_DISPATCH_STARTIO
PNP_HARNESS
PNP_HARNESS_SMALL
PNP_HARNESS_UNLOAD