Difference between revisions of "Software"

From Numerical Transition Systems
Jump to: navigation, search
Line 1: Line 1:
* [http://www.fit.vutbr.cz/research/groups/verifit/tools/trace_inclusion/ TRACER] a tool for checking trace inclusion between infinite state systems
+
* [http://www.fit.vutbr.cz/research/groups/verifit/tools/includer/ all_included] a tool for checking trace inclusion between infinite state systems
 
* [http://www.fit.vutbr.cz/research/groups/verifit/tools/slide/ SLIDE] an entailment checker for Separation Logic with Inductive DEfinitions
 
* [http://www.fit.vutbr.cz/research/groups/verifit/tools/slide/ SLIDE] an entailment checker for Separation Logic with Inductive DEfinitions
 
* [[Flata|FLATA]] a tool for the analysis of counter automata
 
* [[Flata|FLATA]] a tool for the analysis of counter automata

Revision as of 18:26, 22 October 2015

  • all_included a tool for checking trace inclusion between infinite state systems
  • SLIDE an entailment checker for Separation Logic with Inductive DEfinitions
  • FLATA a tool for the analysis of counter automata
  • ARTMC a tool for the verification of programs with complex pointer structures
  • L2CA converts programs with lists into counter automata
  • dSPIN an extension of the model checker SPIN
  • BANDERA project home page
  • JCAT a deadlock detection tool for Java(TM) multithreading programs
  • JSUIF a program internal representation support library entirely written in Java