Difference between revisions of "Software"

From Numerical Transition Systems
Jump to: navigation, search
 
(7 intermediate revisions by the same user not shown)
Line 1: Line 1:
 +
* [https://github.com/timothy-king/CVC4SepLogic CVC4SepLog] SMT solver for quantifier-free ground Separation Logic over unrestricted data theories
 +
* [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
 
* [[Flata|FLATA]] a tool for the analysis of counter automata
 
* [[Flata|FLATA]] a tool for the analysis of counter automata
* ARTMC a tool for the verification of programs with complex pointer structures
+
* [http://www.fit.vutbr.cz/research/groups/verifit/tools/artmc ARTMC] a tool for the verification of programs with complex pointer structures
* L2CA converts programs with lists into counter automata
+
* [http://www-verimag.imag.fr/~async/L2CA/l2ca.html L2CA] converts programs with lists into counter automata
* dSPIN an extension of the model checker SPIN
+
* [http://www-verimag.imag.fr/~iosif/dspin/index.html dSPIN] an extension of the model checker SPIN
* BANDERA project home page
+
* [http://bandera.projects.cis.ksu.edu BANDERA] project home page
* JCAT a deadlock detection tool for Java(TM) multithreading programs
+
* [http://www-verimag.imag.fr/~iosif/jcat/ JCAT] a deadlock detection tool for Java(TM) multithreading programs
* JSUIF a program internal representation support library entirely written in Java
+
* [http://www.dai-arc.polito.it/dai-arc/manual/tools/yav/jsuif/index.html JSUIF] a program internal representation support library entirely written in Java
* YAV yet another verifier for Java(TM) concurrent programs
+

Latest revision as of 09:37, 19 May 2016

  • CVC4SepLog SMT solver for quantifier-free ground Separation Logic over unrestricted data theories
  • 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