Tools

Category	Tool	Subproject
Core algorithms	AIGSolve	S1
	antom	H1/2
	CIP	H1/2
	DBA Minimizer	S1
	FlowSim	S3
	H-PILoT	R1, H3
	HySAT-II	H1/2
	IncQuBE	S1
	iSAT	H1/2
	iSAT-Craig	H1/2
	iSAT-LP	H1/2
	iSAT-parallel (Picoso)	H1/2
	iSAT-ODE	H1/2
	MiraXT	H1/2
	Mira-Craig	H1/2
	NBWMinimizer	S1
	PaQuBE	S1
	QMiraXT	S1
	Quaig	S1
	SiSAT	H1/2
	SmtInterpol	R1
	SPASS(LA)	H1/2, S2
	SPASS(NLA)	H1/2
Model reduction	ASTRA	S2
	closure	S2
	DBA Minimizer	S1
	dcs2gts	S2
	DES	S3
	hiralysis	S2
	hiralyse	S2
	MCSI	S3
	MTS	S2
	NBWMinimizer	S1
	RESY	S1
	SARMC	S2
	sigref	S3
	SPASS-FPTA	S2
Data structures for symbolic state representation	AIGPP	S1
Data structures for symbolic state representation	LinAIG	H3
Systems of systems / blackbox tools	bb	S3
	Bohne	S2
	bounce	S1, H1/2
	MIND	S1
	timemachine	S1
Model checker for hard & soft real-time systems	cgs	R2
	fsmtMC	S1
	INFAMY	S3
	Mcta	R3
	Modest Toolset	S2
	MRMC	S3
	PARAM	S3
	ProHVer	S3
	SHAVE	H4
	SLAB	R1
	SYNTHIA	S1
	ta2fsmt	S1
	timemachine	S1
	wcet_lp	R2
Model checker / solver for probabilistic systems	bb	S3
	DES	S3
	Geobound	S3
	INFAMY	S3
	lter	S3
	MCSI	S3
	Modest Toolset	S2
	MRMC	S3
	PARAM	S3
	PASS	S3
	ProHVer	S3
	SiSAT	H1/2
	SHAVE	H4
	SPASS-FPTA	S2
	(S)SBMC	S3
Model checker / solver for hybrid systems	fomc	H3
	HSolver	H1/2
	HySAT-II	H1/2
	iSAT	H1/2
	iSAT-Craig	H1/2
	iSAT-LP	H1/2
	iSAT-ODE	H1/2
	iSAT-parallel (Picoso)	H1/2
	ProHVer	S3
	SiSAT	H1/2
	SPASS(LA)	H1/2, S2
	SPASS(NLA)	H1/2
	Stabhyli	H4
Synthesis tools	Unbeast	S1
Synthesis tools	SYNTHIA	S1
Graphical specification tools	Syspect	R1
Theorem prover for hybrid systems	KeYmaera	H3
	SPASS(LA)	H1/2, S2
	SPASS(NLA)	H1/2
	SPASS-FPTA	S2
Real-time analysis methods for hardware architectures	ORCA-RT	R2
Real-time analysis methods for hardware architectures	VHDL Timing Model Derivation Toolset	R2

Automatic Verification And Analysis of Complex Systems