SENS Software Tools

Alloy - an object modelling notation that is compatible with development approaches such as UML, Catalysis, Fusion, OMT and Syntropy, strongly influenced by the Z specification language.

Argos - an imperative synchronous language with verification support.

Bandera - a model checking tool for java programs

CADP - Caesar/Aldebaran tools for the verification of concurrent systems

CWB-NC - The Concurrency Workbench of North Carolina, which includes a LOTOS interface and diagnostic information.

DOME - (Domain Modeling Environment) DOME is an extensible collection of integrated model-editing, meta-modeling, and analysis tools.

Larch - family of languages and tools supporting a two-tiered definitional style of specification.

LDE - (Linux Disk Editor) a disk editor for linux, originally written to help recover deleted files.

LOTOS - (Language of Temporal Ordering Specifications)

ROSE - Rational Rose is a model-driven development tool using UML and is part of Rational Software's comprehensive and fully integrated solution designed to meet today's software development challenges.

SCR - (Software Cost Reduction), a tabular notation for specifying requirements and tools for creating and analyzing requirements specifications.

SMV - (Symbolic Model Verifier) model checker for finite-state systems, using the specification language CTL (Computation Tree Logic), a propositional branching-time temporal logic.

Spark - a high-integrity subset of the Ada programming language.

Specware - a next-generation environment supporting the design, development and automated synthesis of scalable, correct-by-construction software.

SPIN - an automated verification tool (model checker), using PROMELA (PROcess MEta LAnguage), a language loosely based on CSP, for finite state systems, such as protocols or validation models of distributed systems, developed at Bell Laboratories.