SRI International

Computer Science Laboratory

The GitHub Projects.

Modeling and Reasoning Tools


Yices 2 is an SMT solver that supports both linear and nonlinear arithmetic.

Timed Intruder

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

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.

Software Analysis Tools

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.

Secure Networking


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.

Security-Enhanced Floodlight

SE-Floodlight is a software extension to the BigSwitch Floodlight controller, providing role-based authorization and strong security constraints enforcement.

SDN Security Actuator

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.

Hidden Service Forum Spider

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.

Cognitive Systems


Semantically Enabled Automated Assessment in Virtual Environments.


bRIGHT is a new human-machine interaction paradigm to increase efficiency and effectiveness for users that are cognitively loaded and heavily tasked.