
DISCOVERER
 Referenced in 58 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...

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

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 120 articles
[sw07714]
 optionally infers some invariants in the given Boogie program, and then generates verification conditions that...

AutoGraphiX
 Referenced in 142 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 157 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 7 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...

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

Daikon
 Referenced in 44 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...

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...

ellipticcovers.lib
 Referenced in 11 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...

ODEtools
 Referenced in 12 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...

Booster
 Referenced in 6 articles
[sw33291]
 allowing Booster to efficiently generate required quantified safe inductive invariants attesting the safety...

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...