Experimental Results of KLEE

RTC Benchmark
Model Lines of Code Violated Properties Paths Explored Total Instructions Runtime Total
Hardware/Software 49119 N/A N/A N/A Timeout
Hardware/Software (unfixed) 49119 N/A N/A N/A Timeout
QEMU Hardware 1567 N/A N/A N/A Timeout
QEMU Hardware (unfixed) 1567 1 1 7227 1s


I2C Benchmark
Model Lines of Code Violated Properties Paths Explored Total Instructions Runtime Total
Hardware/Software 48946 N/A N/A N/A Compilation fail
Hardware/Software (unfixed) 48946 N/A N/A N/A Compilation fail
QEMU Hardware 772 None 1 5470 1s
QEMU Hardware (unfixed) 772 10 1 2896 1s


ETHOC Benchmark
Model Lines of Code Violated Properties Paths Explored Total Instructions Runtime Total
Hardware/Software 2131 None 25 9960 24s
Hardware/Software (unfixed) 2131 None 25 9960 27s
QEMU Hardware 950 None 1 4035 1s