• DISCOVERER

  • Referenced in 55 articles [sw07719]
  • solving itself, termination analysis and invariant generation of programs, and reachability computation of hybrid systems...
  • AIDA

  • Referenced in 58 articles [sw11535]
  • explore algebra of differential invariants: computation of generating sets of invariants, rewritings, syzygies, and their...
  • InvGen

  • Referenced in 15 articles [sw09780]
  • InvGen: An Efficient Invariant Generator. In this paper we present InvGen, an automatic linear arithmetic ... invariant generator for imperative programs. InvGen’s unique feature is in its use of dynamic ... analysis to make invariant generation order of magnitude more efficient...
  • Boogie

  • Referenced in 118 articles [sw07714]
  • optionally infers some invariants in the given Boogie program, and then generates verification conditions that...
  • CIRR

  • Referenced in 32 articles [sw12618]
  • large, iterative methods are used to generate an invariant subspace that contains the desired eigenvectors...
  • AutoGraphiX

  • Referenced in 133 articles [sw06137]
  • which could also be considered as an invariant). From this main capability, some information ... could be extracted and conjectures may be generated automatically or found by the researcher...
  • KANT/KASH

  • Referenced in 155 articles [sw00481]
  • user with the means to compute many invariants of F. It is possible to solve ... Furthermore subfields of F can be generated and F can be embedded into an overfield...
  • PKind

  • Referenced in 6 articles [sw21027]
  • easily accommodate the incorporation of incremental invariant generators to enhance basic k-induction. We describe ... safety properties and, due to incremental invariant generation, also considerably increases the number of provable...
  • HMC

  • Referenced in 7 articles [sw09867]
  • type structure of the functional program to generate a set of logical refinement constraints whose ... simple first-order imperative program and an invariant that holds iff the constraints ... satisfiable. Finally, it uses an invariant generator for first-order imperative programs to discharge...
  • c2i

  • Referenced in 6 articles [sw19488]
  • describe a general framework c2i for generating an invariant inference procedure from an invariant checking ... checker and a language of possible invariants, c2i generates an inference procedure that iteratively invokes ... phase uses randomized search to discover candidate invariants and the validate phase uses the checker ... actual invariant. To demonstrate the applicability of c2i , we use it to generate inference procedures...
  • Daikon

  • Referenced in 43 articles [sw04319]
  • easy to extend Daikon to other applications. Invariants can be useful in program understanding ... Daikon’s output has been used for generating test cases, predicting incompatibilities in component integration...
  • Aligator.jl

  • Referenced in 3 articles [sw26257]
  • Aligator.jl - a Julia package for loop invariant generation. We describe the Aligator.jl software package ... automatically generating all polynomial invariants of the rich class of extended P-solvable loops with...
  • BRISK

  • Referenced in 16 articles [sw29764]
  • BRISK: Binary robust invariant scalable keypoints. Effective and efficient generation of keypoints from an image...
  • Valigator

  • Referenced in 3 articles [sw00994]
  • verification tool with bound and invariant generation. We describe Valigator, a software tool for imperative ... automatically generating and proving verification conditions and, most importantly, for automatically inferring loop invariants...
  • ODEtools

  • Referenced in 11 articles [sw09257]
  • infinitesimal symmetry generator; the construction of the most general invariant first-order ODE under given...
  • Lingva

  • Referenced in 3 articles [sw13645]
  • experiments show that Lingva can automatically generate quantified invariants, possibly with alternation of quantifiers, over...
  • ellipticcovers.lib

  • Referenced in 8 articles [sw20805]
  • approach has the advantage that all involved invariants are easy to compute. Furthermore ... model side (i.e., the generating function of Gromov-Witten invariants) in terms...
  • QuIt

  • Referenced in 1 article [sw29333]
  • partial correctness verification, termination analysis and invariant generation. For doing so, we express the loop...
  • JKind

  • Referenced in 1 article [sw21029]
  • property directed reachability, and template-based invariant generation. Downloads: JKind is written in Java...
  • JSNice

  • Referenced in 1 article [sw37814]
  • context of “big code” including invariant generation, decompilation, synthesis and others...