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

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

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

VHDL Timing Model Derivation Toolset

R2