Subproject

Tool

Categories

R1

H-PILoT

Core algorithms

SLAB

Model checker for hard & soft real-time systems

SmtInterpol

Core algorithms

Syspect

Graphical specification tools

R2

cgs

Model checker for hard & soft real-time systems

ORCA-RT

Real-time analysis methods for hardware architectures

VHDL Timing Model Derivation Toolset

Real-time analysis methods for hardware architectures

wcet_lp

Model checker for hard & soft real-time systems

R3

Mcta

Model checker for hard & soft real-time systems

S1

AIGPP

Data structures for symbolic state representation

AIGSolve

Core algorithms

bounce

Systems of systems / blackbox tools

DBA Minimizer

Core algorithms,

Model reduction

fsmtMC

Model checker for hard & soft real-time systems

incQuBE

Core algorithms

MIND

Systems of systems / blackbox tools

NBWMinimizer

Core algorithms,

Model reduction

PaQuBE

Core algorithms

QMiraXT

Core algorithms

Quaig

Core algorithms

RESY

Model reduction

SYNTHIA

Synthesis tools,

Model checker for hard & soft real-time systems

ta2fsmt

Model checker for hard & soft real-time systems

timemachine

Systems of systems / blackbox tools,

Model checker for hard & soft real-time systems

Unbeast

Synthesis tools

S2

ASTRA

Model reduction

Bohne

Systems of systems / blackbox tools

closure

Model reduction

dcs2gts

Model reduction

hiralysis

Model reduction

hiralyse

Model reduction

Modest Toolset

Model checker for hard & soft real-time systems,

Model checker / solver for probabilistic systems

MTS

Model reduction

PASS

Model checker / solver for probabilistic systems

SARMC

Model reduction

SPASS(LA)

Core algorithms,

Model checker / solver for hybrid systems,

Theorem prover for hybrid systems

SPASS-FPTA

Model reduction,

Model checker / solver for probabilistic systems,

Theorem prover for hybrid systems

S3

bb

Systems of systems / blackbox tools,

Model checker / solver for probabilistic systems

DES

Model reduction,

Model checker / solver for probabilistic systems

FlowSim

Core algorithms

Geobound

Model checker / solver for probabilistic systems

INFAMY

Model checker for hard & soft real-time systems,

Model checker / solver for probabilistic systems

lter

Model checker / solver for probabilistic systems

MCSI

Model reduction,

Model checker / solver for probabilistic systems

MRMC

Model checker for hard & soft real-time systems,

Model checker / solver for probabilistic systems

PARAM

Model checker for hard & soft real-time systems,

Model checker / solver for probabilistic systems

PASS

Model checker / solver for probabilistic systems

ProHVer

Model checker for hard & soft real-time systems,

Model checker / solver for probabilistic systems,

Model checker / solver for hybrid systems

sigref

Model reduction

(S)SBMC

Model checker / solver for probabilistic systems

H1/2

antom

Core algorithms

bounce

Systems of systems / blackbox tools

CIP

Core algorithms

HSolver

Model checker / solver for hybrid systems

HySAT-II

Core algorithms,

Model checker / solver for hybrid systems

iSAT

Core algorithms,

Model checker / solver for hybrid systems

iSAT-Craig

Core algorithms,

Model checker / solver for hybrid systems

iSAT-LP

Core algorithms,

Model checker / solver for hybrid systems

iSAT-parallel (Picoso)

Core algorithms,

Model checker / solver for hybrid systems

iSAT-ODE

Core algorithms,

Model checker / solver for hybrid systems

MiraXT

Core algorithms

Mira-Craig

Core algorithms

SiSAT

Core algorithms,

Model checker / solver for probabilistic systems,

Model checker / solver for hybrid systems

SPASS(LA)

Core algorithms,

Model checker / solver for hybrid systems,

Theorem prover for hybrid systems

SPASS(NLA)

Core algorithms,

Model checker / solver for hybrid systems,

Theorem prover for hybrid systems

H3

fomc

Model checker / solver for hybrid systems

H-PILoT

Core algorithms

KeYmaera

Theorem prover for hybrid systems

LinAIG

Data structures for symbolic state representation

H4

SHAVE

Model checker for hard & soft real-time systems,

Model checker / solver for probabilistic systems

Stabhyli

Model checker / solver for hybrid systems