Multi-Property Verification

A detailed comparison of checking several properties simultaneously (“Multi”) compared to checking each property in a separate verification run (“Single”). The table is ordered by the speedup archived by checking properties simultaneously. The numbers for checking each property separately represent the maximum value of one of the runs.
Verified
Properties
Abstraction
Predicates
Refinements Reached
States
Analysis
CPU Time (s)
Kernel Module Relevant
Properties
Single Multi Single Multi Single Multi Single Multi Single Multi Speedup
spi-spi-tegra20-slink.c2141400004 9024 907977.014
tty-serial-timbuart.c2141400001 5581 563674.914
net-ethernet-mellanox-mlx5-core-mlx5_core.c214140000513 973513 9782 30018013
staging-iio-magnetometer-hmc5843_core.c214140000623628614.813
input-touchscreen-mms114.c2141400001 3331 338645.212
staging-comedi-drivers-amplc_pci224.c2141400001 6961 701675.512
bcma-bcma.c2141400001 4591 464615.012
input-touchscreen-elo.c2141400001 5231 528665.512
sound-soc-codecs-snd-soc-arizona.c2141400002 8002 805796.612
rtc-rtc-stk17ta8.c2141400001 7041 709705.812
net-wan-hdlc.c2141400001 3301 335615.112
rtc-rtc-m48t59.c2141400002 2792 284756.212
usb-phy-phy-tahvo.c2141400001 2571 262635.312
misc-bh1770glc.c2141400001 6071 612695.812
staging-comedi-drivers-das16m1.c214140000855860625.212
input-gameport-gameport.c314140000906911595.012
mfd-tps65010.c2141400001 7411 746695.812
sound-oss-uart401.c2141400002 3212 326746.312
w1-masters-ds1wm.c2141400002 3992 404746.312
input-touchscreen-ad7879.c214140000963968585.012
tty-goldfish.c3141400001 4161 421645.512
staging-comedi-drivers-pcmuio.c2141400002 4342 439695.912
net-appletalk-ipddp.c2141400002 3002 309675.712
scsi-hv_storvsc.c2141400003 1013 106786.712
md-dm-crypt.c1141400005 9956 0001008.912
input-serio-sun4i-ps2.c2141400001 0991 104595.112
net-netconsole.c2141400001 7491 754635.512
rtc-rtc-isl12057.c2141400001 8891 894726.212
net-ethernet-intel-ixgbevf-ixgbevf.c0141400003 8143 819817.111
tty-serial-altera_uart.c2141400002 0712 076736.411
media-platform-s5p-tv-s5p-mixer.c2141400002 0782 083686.011
iio-light-apds9300.c2141400001 5721 577655.711
staging-media-lirc-lirc_sir.c2141400002 4482 453736.511
gpio-gpio-ml-ioh.c2141400001 2311 236635.611
acpi-acpi_ipmi.c2141400001 9851 990686.111
mmc-host-toshsd.c2141400002 9172 922807.211
sound-usb-snd-usbmidi-lib.c2141400004 8474 852928.311
ata-sata_vsc.c2141400001 8391 844716.511
net-can-sja1000-sja1000.c2141400004 1814 186827.511
sound-oss-uart6850.c2141400001 2501 255605.511
tty-serial-max310x.c2141400004 5444 549918.411
media-rc-sunxi-cir.c2141400001 3231 328605.511
sound-oss-pas2.c2141400005 4075 412857.811
sound-pci-hda-snd-hda-intel.c3141400005 7455 7501009.411
scsi-iscsi_tcp.c2141400002 9702 975756.911
memstick-core-mspro_block.c2141400003 8363 841857.811
firewire-firewire-core.c1141400001 6591 664575.311
rapidio-devices-tsi721_mport.c2141400004 4744 479898.311
net-wireless-iwlegacy-iwl3945.c2141400005 4365 441989.211
sound-pci-snd-intel8x0m.c2141400003 4913 496817.711
sound-pci-snd-atiixp.c3141400006 1326 137908.611
sound-core-seq-snd-seq.c312+212+2151610111 395 20554 6711 0009710
staging-comedi-drivers-cb_pcidas.c2141400001 7611 766696.710
staging-comedi-drivers-addi_apci_1500.c2141400001 8731 878656.410
pcmcia-pd6729.c2141400005 9585 963939.110
sound-soc-codecs-snd-soc-wm0010.c3141400003 9313 936868.410
net-nfc-nci-nci.c21414000011 16111 1661201210
fs-fat-vfat.c2141400006 2416 2461101010
char-mwave-mwave.c21414000010 46910 4741201110
ata-sata_nv.c2141400006 2226 2271101010
tty-serial-sccnxp.c2141400003 4773 482848.410
sound-pci-snd-als4000.c2141400002 7182 723767.79.8
scsi-wd719x.c2141400007 5317 536110119.8
sound-pci-snd-atiixp-modem.c3141400004 1524 157848.69.8
media-platform-s3c-camif-s3c-camif.c2141400002 9372 942828.49.8
sound-pci-snd-via82xx.c21414000013 04813 053110129.7
net-wan-x25_asy.c2141400004 9904 999747.69.6
sound-snd-aloop.c2141400004 7424 747859.09.4
usb-gadget-udc-goku_udc.c21414000014 20314 208130149.4
sound-pci-ice1712-snd-ice1712.c31414000011 48811 493140159.2
sound-pci-snd-als300.c2141400003 6933 698778.78.9
sound-pci-snd-rme32.c21414000013 66413 669100128.6
i2c-busses-i2c-xiic.c2141400006 3476 35298128.0
sound-pci-lola-snd-lola.c21414000019 99520 000150197.9
scsi-esp_scsi.c21414000030 27730 282180237.8
scsi-advansys.c214140000115 267115 272460597.7
staging-comedi-drivers-s626.c21414000021 42121 426130177.6
tty-serial-8250-8250.c11414000018 98418 989170237.5
usb-gadget-udc-net2280.c21414000028 56828 573170237.4
tty-nozomi.c21414000046 44046 445190267.3
net-sunrpc-sunrpc.c5141455116 4244 731130197.0
net-netfilter-ipset-ip_set.c414141010223 1631 92396147.0
media-platform-s5p-g2d-s5p-g2d.c3141422112 8992 90484136.6
mmc-host-sdhci.c2141400004 341 6994 341 70411 0001 6006.4
media-pci-bt8xx-bttv.c314140000104 903104 912610966.4
media-platform-mx2_emmaprp.c313+113+100007 1327 14188146.2
misc-tifm_core.c2141433111 1041 11369126.0
staging-iio-trigger-iio-trig-periodic-rtc.c213+113+100001 5471 55564115.8
sound-soc-intel-sst-snd-intel-sst-core.c3141422228 3348 34396175.6
scsi-cxgbi-cxgb4i-cxgb4i.c2141433115 8895 89883155.5
thermal-thermal_sys.c212+212+200002 9792 99577145.5
iio-adc-xilinx-xadc.c4141477335 7545 76399185.5
media-usb-em28xx-em28xx-v4l.c21414222210 34310 348140255.4
iio-light-tcs3414.c3141444111 9451 95474145.4
staging-iio-light-tsl2x7x_core.c2141466332 0832 09289165.4
media-usb-stk1160-stk1160.c41414292213122 2751 549130245.4
net-ethernet-ec_bhf.c2141466222 4462 45580155.3
iio-proximity-sx9500.c3141455112 5282 53775145.3
scsi-qla1280.c314140000436 071436 0761 2002205.2
video-fbdev-via-viafb.c2141400002 411 0822 411 0876 5001 3005.1
net-netfilter-nfnetlink_queue.c3141477112 3002 30574155.0
input-serio-serio.c3141434121 8581 87374155.0
iio-trigger-iio-trig-interrupt.c213+113+122111 2291 23766135.0
net-usb-smsc95xx.c21414000029 41729 422160344.9
ide-ide-gd_mod.c213+113+122113 5483 55785184.9
iio-light-gp2ap020a00f.c2141455223 3133 32279164.8
net-ethernet-silan-sc92031.c31414682317 42417 579130274.8
media-common-saa7146-saa7146.c2141422115 7935 72898204.8
net-ethernet-realtek-r8169.c01414663369 83969 848350744.7
ipack-carriers-tpci200.c4141489231 6921 69785184.7
xen-xen-acpi-processor.c213+113+11616338 9648 97396224.3
net-ethernet-realtek-8139too.c314141212887 2997 308110264.3
net-wireless-ray_cs.c2141411136929 75930 171180424.2
net-l2tp-l2tp_ip6.c2141478123 4273 43595224.2
watchdog-dw_wdt.c213+113+133114 7954 80371174.2
net-wireless-adm8211.c21414221132 29932 308160374.2
net-netfilter-nfnetlink_log.c213+113+11919223 0982 79684204.2
usb-gadget-function-u_serial.c2141499336 0616 07094234.1
net-dccp-dccp_ipv6.c21414664426 21826 227120304.1
block-nbd.c214142020995 0784 938100254.1
net-ethernet-micrel-ks8851_mll.c4141467357 7737 877100254.0
bluetooth-dtl1_cs.c2141477114 70311 98083214.0
usb-misc-appledisplay.c412+212+2611675 6818 126100263.9
arch-x86-kernel-msr.c31414606112142 9823 46790233.9
net-ipv6-sit.c3141422286717 35328 385140373.9
net-ipv4-netfilter-ip_tables.c212+212+210113429 67937 626150403.8
nfc-st21nfca-st21nfca_i2c.c213+113+11010444 4924 50181223.8
fs-coda-coda.c31414404017173 5883 71592253.7
char-xillybus-xillybus_core.c413+113+119203415 40613 982120333.7
ide-ide-cd_mod.c213+113+1781214 97314 982120343.7
char-pcmcia-cm4040_cs.c214143029665 1075 116110303.6
infiniband-core-rdma_cm.c213+113+16161101021 19521 204130383.5
net-ppp-ppp_synctty.c2141478575 4645 49398283.5
net-wireless-orinoco-orinoco.c01414332232 34832 357140403.5
usb-host-fotg210-hcd.c31414151544329 483329 4926401903.4
hid-hid-picolcd.c21414221136 79636 805130403.4
misc-hpilo.c314142221773 5613 61297293.3
char-tlclk.c41414272711112 2482 27488273.3
staging-dgap-dgap.c314144040111166 22066 1413601103.3
net-ethernet-amd-nmclan_cs.c314149135712 88415 068110343.2
net-wireless-ath-ath10k-ath10k_pci.c21414332287 27587 284230703.2
net-ethernet-realtek-8139cp.c3141410136939 09341 429170523.2
staging-iio-accel-lis3l02dq.c213+113+188779 7929 80193293.2
net-ethernet-smsc-epic100.c31414784619 78720 138140443.1
net-can-can.c414142328784 1524 18893303.1
media-usb-dvb-usb-dvb-usb-cxusb.c213+113+1894744 18744 195150483.1
bluetooth-bluecard_cs.c21414771113 24337 890110363.0
staging-lustre-lustre-mgc-mgc.c214147744107 738107 747290963.0
sound-core-snd.c313+113+12228192113 33612 130150493.0
net-ethernet-tehuti-tehuti.c31414111471159 11559 385220753.0
media-rc-ati_remote.c312+212+21820897 90616 807100353.0
message-fusion-mptsas.c213+113+1342338 67188 019170592.9
net-l2tp-l2tp_eth.c41414917133 0622 76879272.9
crypto-af_alg.c213+113+14950774 5994 60783282.9
net-usb-cdc-phonet.c313+113+119267126 8139 57199342.9
net-can-softing-softing.c31414444416 72716 736140492.9
net-netfilter-nfnetlink.c21414191921212 4632 46894332.9
usb-misc-uss720.c512+212+2692526 40754 180130472.8
media-pci-smipcie-smipcie.c213+113+120208851 24351 251140502.7
net-ethernet-dnet.c31414515139394 4054 414100382.7
net-ethernet-dec-tulip-de2104x.c314142630272928 84834 012170632.6
net-ethernet-fujitsu-fmvj18x_cs.c214142627111311 60312 776120442.6
scsi-mvumi.c41414332245 615110 226200802.5
misc-phantom.c413+113+12221887 1015 098100422.5
watchdog-w83977f_wdt.c213+113+1554416 63016 638100412.5
staging-iio-meter-ade7758.c213+113+1141410103 4853 49398422.4
scsi-initio.c2141400003 680 1203 680 1293 6001 5002.4
net-ethernet-xircom-xirc2ps_cs.c21414895865 46368 960210912.4
isdn-hardware-mISDN-w6692.c31414331178 961172 664200842.3
net-wan-sbni.c21414221120 02173 954120532.3
net-ethernet-3com-3c589_cs.c314141314101416 61949 701120552.3
net-decnet-decnet.c213+113+140411718989 205718 8831 9008302.3
staging-media-lirc-lirc_sasem.c311+311+31616101014 95130 314120522.2
block-nvme.c313+113+10000438 309438 3964101802.2
watchdog-pc87413_wdt.c213+113+1443311 51811 52683382.2
net-usb-usbnet.c413+113+1352321 30543 540120562.2
scsi-ch.c314143534886 6906 699120572.1
staging-lustre-lustre-lmv-lmv.c2141471712222109 696109 7056703302.1
usb-host-hwa-hc.c21414171722225 4625 47086432.0
net-ieee802154-ieee802154_socket.c314141114499 2229 287130662.0
input-mousedev.c313+113+116235713 69019 404120632.0
kernel-locking-locktorture.c311+311+3443316 17796 318130691.9
net-wireless-p54-p54usb.c313+113+1232618199 0609 38893521.8
atm-iphase.c21414221169 418274 6422201201.8
scsi-ips.c114145522143 4243 4196203601.7
sound-core-snd-timer.c312+212+22630212052 48673 4902201301.7
media-usb-stkwebcam-stkwebcam.c313+113+1352438 45570 1591601001.5
fs-hfsplus-hfsplus.c213+113+15511111 981 4372 029 8492 1001 4001.5
net-ethernet-amd-amd8111e.c314147946127 617128 2022401601.5
infiniband-hw-ocrdma-ocrdma.c413+113+130461924196 463207 9623702601.5
fs-f2fs-f2fs.c4131445625961-92 0221 8001 300-
net-atm-br2684.c413+113+168498 37913 84399701.4
net-wireless-ath-ath6kl-ath6kl_usb.c314142538576424 01324 3372201601.4
staging-media-lirc-lirc_imon.c311+311+32929273210 54423 4041501101.3
sound-core-seq-oss-snd-seq-oss.c313+113+122221515186 906186 9143002401.3
block-mtip32xx-mtip32xx.c413+113+128281010234 948402 1143703001.2
net-ethernet-neterion-s2io.c3141414211926456 745460 0139908201.2
media-usb-usbtv-usbtv.c411+311+3306222239 55923 1301201001.2
net-wireless-ath-carl9170-carl9170.c512+212+222361730841 4704 521 4442 6002 2001.2
usb-core-usbcore.c81+10+1871392337--12 00013 000-
net-irda-sir-dev.c313+113+14040363629 50129 509140150.95
fs-nilfs2-nilfs2.c30+10+19696113113--13 00013 000.95
ata-libata.c20+10+11111--13 00013 000.94
scsi-gdth.c4008856--13 00013 000.94
net-ethernet-intel-e1000-e1000.c3000000--13 00014 000.93
net-wireless-b43legacy-b43legacy.c3000000--13 00014 000.93
net-ethernet-intel-e100.c314145656106106204 255209 9511 1001 300.81
net-atm-lec.c312+212+21730164352 569344 853180230.78
net-hyperv-hv_netvsc.c2141434348484100 790100 799490640.77
net-netfilter-nf_conntrack_netlink.c114142525202033 16433 169510710.72
net-wireless-orinoco-orinoco_usb.c312+212+242431822374 386993 899300450.68
watchdog-f71808e_wdt.c213+113+137372020385 794385 802580860.67
mfd-rtsx_usb.c213+113+12530395024 9968 690200320.64
net-wireless-libertas_tf-libertas_tf_usb.c213+113+11218222914 32131 714130200.63
net-ethernet-intel-igb-igb.c411013331949--7 50013 000-
input-misc-uinput.c214141616676718 18318 192210360.57
block-paride-pg.c21414999910610673 68773 696300540.55
scsi-st.c411+10+11218510--7 50014 000-
net-ethernet-3com-3c59x.c31414141712171 057 9782 320 3128601 600.55
net-wireless-hostap-hostap_cs.c2131425432439-498 7991 8003 200-
net-bridge-bridge.c31414395053831 348 4455 621 7491 7003 300.50
net-ethernet-sun-cassini.c4141421331532542 6111 371 9335701 200.49
net-can-usb-usb_8dev.c313+113+1183411185 7809 103110240.45
usb-misc-iowarrior.c311+311+32128546464 17892 701210490.42
media-pci-bt8xx-dst_ca.c212+212+255493547 83779 343190500.38
input-mouse-synaptics_usb.c313+113+110812745579 9823 978210550.38
nfc-pn533.c312+212+266734548178 912338 432340940.36
net-can-usb-kvaser_usb.c213+113+11743103010 45723 262120370.32
media-usb-b2c2-b2c2-flexcop-usb.c212+212+22848395910 52984 384110380.28
net-wireless-libertas-libertas.c2130312322--3 00013 000-
net-ethernet-chelsio-cxgb4vf-cxgb4vf.c21313+16711849128-861 3401 2005 300-
net-usb-hso.c4110156234155233--2 80013 000-
media-rc-streamzap.c21214122195118148-2 7311 9009 300-
media-usb-msi2500-msi2500.c411+10+31671872531--1 90013 000-
usb-gadget-legacy-gadgetfs.c31207194225429--1 90013 000-
block-floppy.c013035652151--1 80013 000-
net-wireless-mwl8k.c413+10+174341 468 537-1 80014 000-
net-can-usb-ems_usb.c212+212+25069699840 80680 0952902 400.12
staging-vt6656-vt6656_stage.c412+10+1224728103--1 40013 000-
net-ethernet-atheros-atl1c-atl1c.c3130415179177--1 30013 000-
net-ethernet-via-via-velocity.c5130112189111188--1 30013 000-
net-ethernet-intel-ixgb-ixgb.c313044703862--1 30013 000-
net-irda-ali-ircc.c4141425286430645 198376 9324905 300.092
media-usb-pwc-pwc.c411+30+255631001381 148 104-1 10013 000-
net-fddi-defxx.c3130107187104184--1 10013 000-
mfd-dln2.c313+113+18497647896 456227 5663203 700.086
misc-genwqe-genwqe_card.c21308614669129--1 10013 000-
net-ethernet-sis-sis900.c313097123326402--1 10013 000-
usb-misc-usbtest.c512+212+220321220169 6958 058 2732703 200.083
isdn-gigaset-bas_gigaset.c413+113+135647511915 934884 6671904 500.043