

System 
Description 

LTL 

Spin 

Check Linear Prepositional temporal logic properties Transfer linear prepositional temporal logic to buchi automata. Wide used model checker 

Complexity is N*2^{O(n)}. in which N is the total state of the system and n is the number of sub formula of the prepoerty we want to check 

System input language: Promela(Process or Protocol Meta Language). Have declarations. Variables, finite length array, Symbolic constants, structure, processes, etc, so you can build a finite state machine/kripke structure out of it. 

Property
language: verification
of linear time temporal constraints; either with Promela neverclaims or by directly
formulating the constraints in temporal logic 

Common
used verifier, have support 




3VMC is a tool for analysis and verification of concurrent systems. 3VMC is geared towards verification of concurrent software, it supports dynamic allocation of objects and threads and does not put an a priori bound on the number of allocated objects and threads. 3VMC provides a powerful abstraction mechanism based on 3valued logic. 3VMC is an extension of the TVLA framework. 

Main features:
· Desired properties can be formulated as assertions or as a general Buchi automata. 

System input language: modeled using transition systems. The transition system is specified using the TVM language. 

For academic only. No support 








CTL CTL* 

Rainbow 
http://www.cs.man.ac.uk/fmethods/projects/AHVPROJECT/ahvproject.html 

Check CTL* Prepositional temporal logic properties Using game to do the checking Can’t handle conditions while transfer from state to state 

System input language: modeled using kripke structure, no conditions while transfer from state to state 

Property
language: verification
of branching time temporal constraints; by directly formulating the
constraints in temporal logic CTL 


SMV 

a symbolic model checker
for CTL, support concurrency. handles prepositional CTL, 

System input language: The system is described by a highlever description program
language. Which is transferred into OBDD(ordered binary decision diagram),
OBDD will make the verification easy. no input is involved. 

Property
language: verification
of branching time temporal constraints; by directly formulating the
constraints in prepositional temporal logic CTL. The CTL properties write as
it is CTL formula following the keyword ”SPEC”. 

SMV was able to determine CTL formula is violated, and to produce a counterexample to show why this happens 

* 
SF2SMV 

An practice extension to SMV Formal Verification of Stateflow Diagrams(which is build by Matlab 6.0) Using SMV. Sf2smv transforms Matlab Stateflow diagram to SMV model file for model checking purpose(using Matlab stateflow toolbox—simulate finite state machine). 

Can
check properties like:


System input language: modeled using Matlab’s Stateflow toolbox. Sf2smv transforms Matlab Stateflow diagram to SMV model file for
model checking purpose(using Matlab stateflow toolbox—simulate finite state
machine). Can handle conditions while transfer from
state to state, have actions, input, is eventdriven. Have input
variables.(but you need to supply the range) 

Property
language: verification
of branching time temporal constraints; by directly formulating the
constraints in prepositional temporal logic CTL. The CTL properties write as
it is CTL formula following the keyword ”SPEC”. 

Restrictions
Function call actions and complex mathematical expression are not supported. 






FO 

3TAP 

Check First order logic properties. Can’t check temporal logic at all 


SVC 

The Stanford Validity Checker (SVC for short) is a research tool to check the validity of formulas expressed in a subset of firstorder logic. SVC is an attractive tool for formal verification because of its efficient and automatic decision procedures. 

Can’t check temporal logic at all 











FOTL 

Mind 

Three Value logic analyzer, it is a program correctness checker. 


MONA 

TVLA is a “yacc”like framework for automatically constructing staticanalysis algorithms from operational semantics, where the operational semantics are specified using logic formulae. 

The system ‘s description is based on firstorder predicate logic with transitive closure. An additional input to TVLA is an abstract representation of all the memory state at the beginning of the analyzer program. The input to TVLA consists of two fi 

Three value: meaning sometimes it will say “I don’t know” 



System input language: firstorder logic with transitive
closure. TVLA only supports predicates of arity <3; such logical structure can be thought of as directed graph. 

Property language: output descriptor. Properties can be extracted by evaluating formulae with transitive closure and equality, but without function symbols and constant symbols 

System theoretical base: the
embedding theorem


Reference:


For academic only. No support 

Used in shape analysis 

No temporal logic used. But can
temporal logic being express by secondorder logic? 


WS1S 


Theory base for of MONA. 

Despite its name, WS1S is a simple and natural notation. Being a variation of firstorder logic, WS1S is formalism with quantifiers and Boolean connectives. Its interpretation, however, is tied to arithmetic somewhat weakened to keep the formalism decidable. In WS1S, firstorder variables denote natural numbers, which can be compared and subjected to addition with constants. WS1S also allows secondorder variables while remaining decidable; each such variable is interpreted as a finite set of numbers. 

WS1S and its generalization WS2S [TW68, Don70], which is interpreted over the infinite binary tree, can be used to express problems ranging from hardware verification to formal linguistics. Unfortunately, the space and time requirements for translating formulas to automata have been shown to be nonelementary 



TVLA 
Three Value logic analyzer, it is a program correctness checker. 

TVLA is a “yacc”like framework for automatically constructing staticanalysis algorithms from operational semantics, where the operational semantics are specified using logic formulae. 

The system ‘s description is based on firstorder predicate logic with transitive closure. An additional input to TVLA is an abstract representation of all the memory state at the beginning of the analyzer program. 



The input to TVLA consists of two fi 

Three value: meaning sometimes it will say “I don’t know” 

Output: a finite set of all structures that satisfied with all the operational semantic and properties. 

System input language: firstorder logic with transitive
closure. TVLA only supports predicates of arity <3; such logical
structure can be thought of as directed graph. 

Property
language:
output descriptor. Properties can be extracted by evaluating formulae with
transitive closure and equality, but without function symbols and constant
symbols 

System theoretical base: the
embedding theorem Any formula that evaluates to a definite value in a 3valued structure
evaluate to the sane value in all the 2valued structures embedded into that
structure. 

Reference:


For academic only. No support 

Used in shape analysis 
