Yices 2 is an SMT solver that supports both linear and nonlinear arithmetic.
TimedIntruder is a tool for modeling and analysis of cyber-security protocols. The tool supports symbolic search for attacks.
Synudic is a paradigm for program synthesis that relies on dual interpretation to encode nonfunctional requirements and prune the synthesis search space.
Sunflower is an integrated development environment (IDE) for ontologies, rules, and reasoning.
Sally is an SMT-based model checker for infinite state systems.
SAL is a model-checking toolbox for modeling and verifying finite and infinite state-transition systems.
PVS is a verification system: that is, a specification language integrated with support tools and a theorem prover.
The Probabilistic Consistency Engine is a probabilistic reasoning engine based on Markov Chain Monte Carlo sampling.
Pathway Logic (PL) is a framework based on rewriting logic for developing and analyzing executable models of cellular processes.
Maude is a high performance implementation of rewriting logic, a simple logic for modeling concurrent, distributed systems.
The Evidential Tool Bus is used to create and maintain evidence-based arguments, for example, for assurance cases.
Fully Automated Analysis Framework for LLVM-based Languages.
To produce LLVM bitcode from an arbitrary C or C++ library or executable, use wllvm.
Object Culling and Concretization for Assurance Maximization.
JayHorn is a software model checking tool for Java.
Do-Like-Javac (or DLJC) monitors ant, maven, gradle, etc builds to record the used source files and classpath, and the generated class files.
Automatic detection of inconsistency bugs in Java code.
Stegotorus is a network proxy that disguises tor traffic as ordinary http to penetrate nation state firewalls, especially those that block tor traffic, or even https traffic.
Tool for flow-by-flow contextual security analysis.
SE-Floodlight is a software extension to the BigSwitch Floodlight controller, providing role-based authorization and strong security constraints enforcement.
The SDN Security Actuator is a middle-ware abstraction service that enables legacy INFOSEC security products and technology to easily integrate into an OpenFlow network stack.
OpenFlow security features that can be integrated at all layers of the OpenFlow stack.
HSProbe looks for Hidden Service domains on the Dark Web.
Dark Crawler that grabs content from Hidden Services.
A content-based networking solution that provides network services and transport architectures required for efficient, transparent distribution of content in mobile ad hoc networks.
