Detail page for tipfixpoint family


	Submitter:	Armin Biere

	Suite:	Biere

	Domain:	Formal Verification

	Description:	Backward fixpoint computation for safety properties of the TIP benchmarks. Details are available in Armin Biere, Toni Jussila. "Compressing BMC Encodings with QBF." BMC’06 (2006): 27.

	Number of instances:	446

	Results:	2020 - Track 1 2019 - Track 1 2018 - Track 1 2018 - Track 5 2017 - Track 1 2016 - Track 1 2016 - Track 2 2016 - Track 5 2016 - Track 6 2016 - Track 7 2010 - Track 1 2010 - Track 3 2008 - Track 1 2007 - Track 1 2006 - Track 1

	Instances:	cmu.dme1.B-f2 cmu.dme1.B-f3 cmu.dme1.B-f4 cmu.dme2.B-f2 cmu.dme2.B-f3 cmu.dme2.B-f4 cmu.gigamax.B-f2 cmu.gigamax.B-f3 cmu.gigamax.B-f4 cmu.periodic.N-f2 cmu.periodic.N-f3 cmu.periodic.N-f4 eijk.bs1512.S-f2 eijk.bs1512.S-f3 eijk.bs1512.S-f4 eijk.bs3271.S-f2 eijk.bs3271.S-f3 eijk.bs3271.S-f4 eijk.bs3330.S-f2 eijk.bs3330.S-f3 eijk.bs3330.S-f4 eijk.bs3384.S-f2 eijk.bs3384.S-f3 eijk.bs3384.S-f4 eijk.bs4863.S-f2 eijk.bs4863.S-f3 eijk.bs4863.S-f4 eijk.bs6669.S-f2 eijk.bs6669.S-f3 eijk.bs6669.S-f4 eijk.S1196.S-f2 eijk.S1196.S-f3 eijk.S1196.S-f4 eijk.S1238.S-f2 eijk.S1238.S-f3 eijk.S1238.S-f4 eijk.S1423.S-f2 eijk.S1423.S-f3 eijk.S1423.S-f4 eijk.S208.S-f2 eijk.S208.S-f3 eijk.S208.S-f4 eijk.S208c.S-f2 eijk.S208c.S-f3 eijk.S208c.S-f4 eijk.S208o.S-f2 eijk.S208o.S-f3 eijk.S208o.S-f4 eijk.S298.S-f2 eijk.S298.S-f3 eijk.S298.S-f4 eijk.S344.S-f2 eijk.S344.S-f3 eijk.S344.S-f4 eijk.S349.S-f2 eijk.S349.S-f3 eijk.S349.S-f4 eijk.S382.S-f2 eijk.S382.S-f3 eijk.S382.S-f4 eijk.S386.S-f2 eijk.S386.S-f3 eijk.S386.S-f4 eijk.S420.S-f2 eijk.S420.S-f3 eijk.S420.S-f4 eijk.S444.S-f2 eijk.S444.S-f3 eijk.S444.S-f4 eijk.S510.S-f2 eijk.S510.S-f3 eijk.S510.S-f4 eijk.S526.S-f2 eijk.S526.S-f3 eijk.S526.S-f4 eijk.S5378.S-f2 eijk.S5378.S-f3 eijk.S5378.S-f4 eijk.S641.S-f2 eijk.S641.S-f3 eijk.S641.S-f4 eijk.S713.S-f2 eijk.S713.S-f3 eijk.S713.S-f4 eijk.S820.S-f2 eijk.S820.S-f3 eijk.S820.S-f4 eijk.S832.S-f2 eijk.S832.S-f3 eijk.S832.S-f4 eijk.S838.S-f2 eijk.S838.S-f3 eijk.S838.S-f4 eijk.S953.S-f2 eijk.S953.S-f3 eijk.S953.S-f4 irst.dme4.B-f2 irst.dme4.B-f3 irst.dme4.B-f4 irst.dme5.B-f2 irst.dme5.B-f3 irst.dme5.B-f4 irst.dme6.B-f2 irst.dme6.B-f3 irst.dme6.B-f4 ken.flash^01.C-f2 ken.flash^01.C-f3 ken.flash^01.C-f4 ken.flash^02.C-f2 ken.flash^02.C-f3 ken.flash^02.C-f4 ken.flash^03.C-f2 ken.flash^03.C-f3 ken.flash^03.C-f4 ken.flash^04.C-f2 ken.flash^04.C-f3 ken.flash^04.C-f4 ken.flash^05.C-f2 ken.flash^05.C-f3 ken.flash^05.C-f4 ken.flash^06.C-f2 ken.flash^06.C-f3 ken.flash^06.C-f4 ken.flash^07.C-f2 ken.flash^07.C-f3 ken.flash^07.C-f4 ken.flash^08.C-f2 ken.flash^08.C-f3 ken.flash^08.C-f4 ken.flash^09.C-f2 ken.flash^09.C-f3 ken.flash^09.C-f4 ken.flash^10.C-f2 ken.flash^10.C-f3 ken.flash^10.C-f4 ken.flash^11.C-f2 ken.flash^11.C-f3 ken.flash^11.C-f4 ken.flash^12.C-f2 ken.flash^12.C-f3 ken.flash^12.C-f4 ken.oop^1.C-f2 ken.oop^1.C-f3 ken.oop^1.C-f4 ken.oop^2.C-f2 ken.oop^2.C-f3 ken.oop^2.C-f4 nusmv.brp.B-f2 nusmv.brp.B-f3 nusmv.brp.B-f4 nusmv.dme1-16.B-f2 nusmv.dme1-16.B-f3 nusmv.dme1-16.B-f4 nusmv.dme2-16.B-f2 nusmv.dme2-16.B-f3 nusmv.dme2-16.B-f4 nusmv.guidance^1.C-f2 nusmv.guidance^1.C-f3 nusmv.guidance^1.C-f4 nusmv.guidance^2.C-f2 nusmv.guidance^2.C-f3 nusmv.guidance^2.C-f4 nusmv.guidance^3.C-f2 nusmv.guidance^3.C-f3 nusmv.guidance^3.C-f4 nusmv.guidance^4.C-f2 nusmv.guidance^4.C-f3 nusmv.guidance^4.C-f4 nusmv.guidance^5.C-f2 nusmv.guidance^5.C-f3 nusmv.guidance^5.C-f4 nusmv.guidance^6.C-f2 nusmv.guidance^6.C-f3 nusmv.guidance^6.C-f4 nusmv.guidance^7.C-f2 nusmv.guidance^7.C-f3 nusmv.guidance^7.C-f4 nusmv.guidance^8.C-f2 nusmv.guidance^8.C-f3 nusmv.guidance^8.C-f4 nusmv.guidance^9.C-f2 nusmv.guidance^9.C-f3 nusmv.guidance^9.C-f4 nusmv.queue.B-f2 nusmv.queue.B-f3 nusmv.queue.B-f4 nusmv.reactor^2.C-f2 nusmv.reactor^2.C-f3 nusmv.reactor^2.C-f4 nusmv.reactor^3.C-f2 nusmv.reactor^3.C-f3 nusmv.reactor^3.C-f4 nusmv.reactor^4.C-f2 nusmv.reactor^4.C-f3 nusmv.reactor^4.C-f4 nusmv.reactor^5.C-f2 nusmv.reactor^5.C-f3 nusmv.reactor^5.C-f4 nusmv.reactor^6.C-f2 nusmv.reactor^6.C-f3 nusmv.reactor^6.C-f4 nusmv.reactor^7.C-f2 nusmv.reactor^7.C-f3 nusmv.reactor^7.C-f4 nusmv.syncarb10^2.B-f2 nusmv.syncarb10^2.B-f3 nusmv.syncarb10^2.B-f4 nusmv.syncarb5^2.B-f2 nusmv.syncarb5^2.B-f3 nusmv.syncarb5^2.B-f4 nusmv.tcas-t^1.B-f2 nusmv.tcas-t^1.B-f3 nusmv.tcas-t^1.B-f4 nusmv.tcas-t^2.B-f2 nusmv.tcas-t^2.B-f3 nusmv.tcas-t^2.B-f4 nusmv.tcas-t^3.B-f2 nusmv.tcas-t^3.B-f3 nusmv.tcas-t^3.B-f4 nusmv.tcas-t^4.B-f2 nusmv.tcas-t^4.B-f3 nusmv.tcas-t^4.B-f4 nusmv.tcas-t^5.B-f2 nusmv.tcas-t^5.B-f3 nusmv.tcas-t^5.B-f4 nusmv.tcas-t^6.B-f2 nusmv.tcas-t^6.B-f3 nusmv.tcas-t^6.B-f4 nusmv.tcas^1.B-f2 nusmv.tcas^1.B-f3 nusmv.tcas^1.B-f4 nusmv.tcas^2.B-f2 nusmv.tcas^2.B-f3 nusmv.tcas^2.B-f4 nusmv.tcas^3.B-f2 nusmv.tcas^3.B-f3 nusmv.tcas^3.B-f4 nusmv.tcas^4.B-f2 nusmv.tcas^4.B-f3 nusmv.tcas^4.B-f4 nusmv.tcas^5.B-f2 nusmv.tcas^5.B-f3 nusmv.tcas^5.B-f4 nusmv.tcas^6.B-f2 nusmv.tcas^6.B-f3 nusmv.tcas^6.B-f4 texas.ifetch1^1.E-f2 texas.ifetch1^1.E-f3 texas.ifetch1^1.E-f4 texas.ifetch1^2.E-f2 texas.ifetch1^2.E-f3 texas.ifetch1^2.E-f4 texas.ifetch1^3.E-f2 texas.ifetch1^3.E-f3 texas.ifetch1^3.E-f4 texas.ifetch1^4.E-f2 texas.ifetch1^4.E-f3 texas.ifetch1^4.E-f4 texas.ifetch1^5.E-f2 texas.ifetch1^5.E-f3 texas.ifetch1^5.E-f4 texas.ifetch1^7.E-f2 texas.ifetch1^7.E-f3 texas.ifetch1^7.E-f4 texas.ifetch1^8.E-f2 texas.ifetch1^8.E-f3 texas.ifetch1^8.E-f4 texas.ifetch1^9.E-f2 texas.ifetch1^9.E-f3 texas.ifetch1^9.E-f4 texas.parsesys^1.E-f2 texas.parsesys^1.E-f3 texas.parsesys^1.E-f4 texas.parsesys^2.E-f2 texas.parsesys^2.E-f3 texas.parsesys^2.E-f4 texas.parsesys^3.E-f2 texas.parsesys^3.E-f3 texas.parsesys^3.E-f4 texas.parsesys^4.E-f2 texas.parsesys^4.E-f3 texas.parsesys^4.E-f4 texas.PI_main^01.E-f2 texas.PI_main^01.E-f3 texas.PI_main^01.E-f4 texas.PI_main^02.E-f2 texas.PI_main^02.E-f3 texas.PI_main^02.E-f4 texas.PI_main^03.E-f2 texas.PI_main^03.E-f3 texas.PI_main^03.E-f4 texas.PI_main^05.E-f2 texas.PI_main^05.E-f3 texas.PI_main^05.E-f4 texas.PI_main^08.E-f2 texas.PI_main^08.E-f3 texas.PI_main^08.E-f4 texas.PI_main^10.E-f2 texas.PI_main^10.E-f3 texas.PI_main^10.E-f4 texas.PI_main^11.E-f2 texas.PI_main^11.E-f3 texas.PI_main^11.E-f4 texas.PI_main^12.E-f2 texas.PI_main^12.E-f3 texas.PI_main^12.E-f4 texas.PI_main^13.E-f2 texas.PI_main^13.E-f3 texas.PI_main^13.E-f4 texas.PI_main^14.E-f2 texas.PI_main^14.E-f3 texas.PI_main^14.E-f4 texas.PI_main^15.E-f2 texas.PI_main^15.E-f3 texas.PI_main^15.E-f4 texas.PI_main^16.E-f2 texas.PI_main^16.E-f3 texas.PI_main^16.E-f4 texas.two_proc^1.E-f2 texas.two_proc^1.E-f3 texas.two_proc^1.E-f4 texas.two_proc^2.E-f2 texas.two_proc^2.E-f3 texas.two_proc^2.E-f4 texas.two_proc^3.E-f2 texas.two_proc^3.E-f3 texas.two_proc^3.E-f4 texas.two_proc^4.E-f2 texas.two_proc^4.E-f3 texas.two_proc^4.E-f4 texas.two_proc^5.E-f2 texas.two_proc^5.E-f3 texas.two_proc^5.E-f4 texas.two_proc^6.E-f2 texas.two_proc^6.E-f3 texas.two_proc^6.E-f4 vis.4-arbit^1.E-f2 vis.4-arbit^1.E-f3 vis.4-arbit^1.E-f4 vis.4-arbit^2.E-f2 vis.4-arbit^2.E-f3 vis.4-arbit^2.E-f4 vis.arbiter.E-f2 vis.arbiter.E-f3 vis.arbiter.E-f4 vis.bakery.E-f2 vis.bakery.E-f3 vis.bakery.E-f4 vis.coherence^1.E-f2 vis.coherence^1.E-f3 vis.coherence^1.E-f4 vis.coherence^2.E-f2 vis.coherence^2.E-f3 vis.coherence^2.E-f4 vis.coherence^3.E-f2 vis.coherence^3.E-f3 vis.coherence^3.E-f4 vis.coherence^5.E-f2 vis.coherence^5.E-f3 vis.coherence^5.E-f4 vis.eisenberg.E-f2 vis.eisenberg.E-f3 vis.eisenberg.E-f4 vis.elevator^1.E-f2 vis.elevator^1.E-f3 vis.elevator^1.E-f4 vis.elevator^2.E-f2 vis.elevator^2.E-f3 vis.elevator^2.E-f4 vis.elevator^3.E-f2 vis.elevator^3.E-f3 vis.elevator^3.E-f4 vis.emodel.E-f2 vis.emodel.E-f3 vis.emodel.E-f4 vis.prodcell^01.E-f2 vis.prodcell^01.E-f3 vis.prodcell^01.E-f4 vis.prodcell^02.E-f2 vis.prodcell^02.E-f3 vis.prodcell^02.E-f4 vis.prodcell^03.E-f2 vis.prodcell^03.E-f3 vis.prodcell^03.E-f4 vis.prodcell^04.E-f2 vis.prodcell^04.E-f3 vis.prodcell^04.E-f4 vis.prodcell^05.E-f2 vis.prodcell^05.E-f3 vis.prodcell^05.E-f4 vis.prodcell^06.E-f2 vis.prodcell^06.E-f3 vis.prodcell^06.E-f4 vis.prodcell^07.E-f2 vis.prodcell^07.E-f3 vis.prodcell^07.E-f4 vis.prodcell^08.E-f2 vis.prodcell^08.E-f3 vis.prodcell^08.E-f4 vis.prodcell^09.E-f2 vis.prodcell^09.E-f3 vis.prodcell^09.E-f4 vis.prodcell^10.E-f3 vis.prodcell^10.E-f4 vis.prodcell^11.E-f2 vis.prodcell^11.E-f3 vis.prodcell^11.E-f4 vis.prodcell^12.E-f2 vis.prodcell^12.E-f3 vis.prodcell^12.E-f4 vis.prodcell^13.E-f2 vis.prodcell^13.E-f3 vis.prodcell^13.E-f4 vis.prodcell^14.E-f2 vis.prodcell^14.E-f3 vis.prodcell^14.E-f4 vis.prodcell^15.E-f2 vis.prodcell^15.E-f3 vis.prodcell^15.E-f4 vis.prodcell^16.E-f2 vis.prodcell^16.E-f3 vis.prodcell^16.E-f4 vis.prodcell^17.E-f2 vis.prodcell^17.E-f3 vis.prodcell^17.E-f4 vis.prodcell^18.E-f2 vis.prodcell^18.E-f3 vis.prodcell^18.E-f4 vis.prodcell^19.E-f2 vis.prodcell^19.E-f3 vis.prodcell^19.E-f4 vis.prodcell^20.E-f2 vis.prodcell^20.E-f3 vis.prodcell^20.E-f4 vis.prodcell^21.E-f2 vis.prodcell^21.E-f3 vis.prodcell^21.E-f4 vis.prodcell^22.E-f2 vis.prodcell^22.E-f3 vis.prodcell^22.E-f4 vis.prodcell^23.E-f2 vis.prodcell^23.E-f3 vis.prodcell^23.E-f4 vis.prodcell^24.E-f2 vis.prodcell^24.E-f3 vis.prodcell^24.E-f4

The Quantified Boolean Formulas Satisfiability Library

Detail page for tipfixpoint family