
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 subﬁelds of F can be generated and F can be embedded into an overﬁeld...

PKind
 Referenced in 6 articles
[sw21027]
 easily accommodate the incorporation of incremental invariant generators to enhance basic kinduction. 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 firstorder imperative program and an invariant that holds iff the constraints ... satisfiable. Finally, it uses an invariant generator for firstorder 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 Psolvable 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 firstorder 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 GromovWitten 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 templatebased 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...