Difference between revisions of "Software"

From Numerical Transition Systems
Jump to: navigation, search
Line 1: Line 1:
* A prototype for checking [http://www.fit.vutbr.cz/research/groups/verifit/tools/trace_inclusion/ trace inclusion] of infinite state systems
+
* [http://www.fit.vutbr.cz/research/groups/verifit/tools/trace_inclusion/ TRACES] 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:59, 19 February 2015

  • TRACES 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