### BYODroid

BYODroid is an
Android-based
implementation of a Secure Meta-Market, allowing to define and enforce
formal "Bring Your Own Device" policies on mobile apps. The theoretical
background of BYODroid can be found in

[SAC2013] and

[IJIS2014], while the experimental
assessment is discussed in

[Computer2014]
and

[WiSec2014].

### AVANTSSAR

The

AVANTSSAR
Platform The AVANTSSAR Validation Platform, an automated toolset
for validating trust and security aspects of service-oriented
architectures. An overview of the AVANTSSAR Platform can be found

here.

### ASASP

ASASP
(short for
Automated Symbolic Analysis of Security Policies) is an implementation
of the analysis techniques for Administrative RBAC (ARBAC) policies. It
implements a symbolic backward reachability analysis to solve user-role
reachability problems. An overview of ASASP can be found

here.

### Eureka

Eureka
is a model checker for sequential software based on the
counterexample-guided abstraction refinement (CEGAR) paradigm. Unlike
many other software model checkers based on the CEGAR paradigm Eureka
analyses arrays precisely. An overview of Eureka can be found

here.

### SMT-CBMC

SMT-CBMC
is a bounded model checker for sequential software. SMT-CBMC reduces
the problem of checking whether an input program has an execution path
of bounded length violating an assertion to the satisfiability of a
formula with respect to a decidable theory. The resulting formula is
fed and solved by a state-of-the-art SMT-solver taken off-the-shelf. An
overview of SMT-CBMC can be found

here.

### AVISPA

The

AVISPA
Tool is a fully automatic analyser for large-scale Internet
security-sensitive protocols. It comprises 4 back-ends implementing a
variety of security protocol verification techniques. An overview of
the AVISPA Tool can be found

here.

### AVISS Tool

The

AVISS Tool is a fully
automatic
security protocol
analyser. It is capable to analyse a large portion of the protocols
collected in the

Clark
& Jacob library of security protocols. An overview of the AVISS
Tool can be found

here.
The AVISS Tool is the predecessor of the AVISPA Tool.

### SATMC

SATMC
(SAT-based Model Checker)
is a bounded model checker for security protocols. SATMC reduces the
problem of checking whether a protocol is vulnerable to attacks of
bounded length to the satisfiability of a propositional formula which
is solved by a state-of-the-art SAT solver taken off-the-shelf. SATMC
is one of the back-ends of the AVISPA Tool. An overview of SATMC can be
found

here.

### TSAT++

TSAT++ is an open
platform for satisfiability
modulo theories (SMT) based on a tight coupling of satisfiability
procedures and a SAT-solver. The current version of TSAT++ supports
Separation Logic (also known as Difference Logic). An overview of
TSAT++ can be found

here.

### RDL

RDL
(Rewrite and Decision Procedures Laboratory). RDL is a fully automatic
tool for formula simplification in a quantifier-free first-order
theories. RDL is based on the Constraint Contextual Rewriting paradigm
and features a tight integration of rewriting and decision procedures.
An overview of RDL can be found

here.