Difference between revisions of "Software"

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

  • A prototype for checking trace inclusion of 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