Temporal Logic
- Temporal Logic
(Stanford Encyclopedia of Philosophy)
- LTL - Linear Time Logic
- CTL
- ITL Interval Temporal Logic
- Computation Tree Logic
- TVL Temporal Logic Verifier
C program verifiers
- Caduceus a Verification Tool for C Programs
- Model Checking @ CMU (Carnegie Mellon University)
- CBMC Bounded Model Checking for ANSI-C
- eureka project home page
- MAGIC Modular Analysis of proGrams In C
- coverity commercial C code checker
- SATABS a verification tool for ANSI-C programs
- caduceus vefirication tool for C programs
- BLAST
Berkeley Lazy Abstraction Software Verification Tool
- Uno a simple tool for source code analysis (Bell Labs)
- VeriSoft automated test/verification system (Bell Labs)
- Eau Claire C program verifier
- BOOP Determines reachability points in a C program
(Graz University of Technology)
- SLAM Debugging System Software via Static Analysis
(Microsoft)
- Unravel Project Program Slicing tool
- SATABS Predicate Abstration with SAT for ANSI-C
- ComFoRT Model Checking Technology
Model Checkers
- Eureka Project Home Page
- WHY The WHY Verification Tool
- CAV Computer Aided Verification (pdf)
- Mocha Exploiting Modularity in Model Checking
- NuSMV new Symbolic Model Verifier
- CIL C Intermediate Language
(Berkeley)
- SPIN Simple Promela INterpreter
(Bell Labs)
- LMC Logic-based Model Checking
(Stony Brook, State University of New York)
- XMC download
- Model Checking online book
(Berkeley)
- Murphi Description Language and Verifier
(Stanford)
- Formal Methods at Bell Laboratories
- PV The Protocol Verifier
(University of Utah)
- Otter an Automated Deduction System
(Argonne National Laboratory)
- Truth a Tool for the Verification of Distributed Systems
(RWTH Aachen)
Computer algebra
- Maxima a computer algebra system
(MIT)
- Axiom
- MuPAD Multi Processing Algebra Data tool - Open computer algebra system
(University of Paderborn)
- Octave Numerical Mathematics Tool
- gnuplot
- GPlot a smart frontend for gnuplot
CCS - Calculus of Communicating Systems
CSP - Communicating Sequential Processes
OAS Ontewerp en Analyse van Systemen (Design and Analsys of Systems)