 |
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)
| Benchmark | Notes | [SRC] | [PLA] | [INS] | [ABS] |
|---|---|---|---|---|---|
| Powerstone |  |
 |
|
|
|
| SNU Real-Time |  |
|
|
|
|
| SNU Real-Time (nondet) | |
|
|
|
|
| NECLA Static Analysis Benchmarks | |
|
|
|
|
| SSH Control Flow (ssh-magic) | |
|
|
|
|
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.
| Harness | Download |
|---|---|
| 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 | |