
VCC
 Referenced in 58 articles
[sw07220]
 program, annotated with function specifications, data invariants, loop invariants, and ghost code, and tries...

Aligator
 Referenced in 8 articles
[sw00029]
 package Aligator for automatically inferring polynomial loop invariants. The package combines algorithms from symbolic summation ... rich class of Psolvable loops. Aligator contains routines for checking the Psolvability ... closed forms of loop variables, computing the ideal of polynomial invariants by variable elimination, invariant...

ABC
 Referenced in 7 articles
[sw09721]
 with symbolic summation techniques to derive loop invariant relations between program variables. Iteration bounds ... obtained from the inferred invariants, by replacing variables with bounds on their greatest values ... bounds express nontrivial polynomial relations over loop variables. We also report on results...

FixBag
 Referenced in 4 articles
[sw10096]
 tool is able to derive both loop invariants and method pre/post conditions via fixpoint analysis...

DynaMate
 Referenced in 2 articles
[sw14286]
 DynaMate: dynamically inferring loop invariants for automatic full functional verification. DYNAMATE is a tool that ... automatically infers loop invariants and uses them to prove Java programs correct with respect ... specification. DYNAMATE improves the flexibility of loop invariant inference by integrating static (proving) and dynamic...

Valigator
 Referenced in 3 articles
[sw00994]
 Valigator: A verification tool with bound and invariant generation. We describe Valigator, a software tool ... most importantly, for automatically inferring loop invariants and bound assertions by means of symbolic summation...

HaLoop
 Referenced in 3 articles
[sw27955]
 features: 1) provide caching options for loopinvariant data access, 2) let users reuse major...

ALICe
 Referenced in 1 article
[sw15036]
 ALICe: A framework to improve affine loop invariant computation. A crucial point in program analysis ... computation of loop invariants. Accurate invariants are required to prove properties on a program ... compare automatic computation techniques of affine loop scalar invariants. It comes with a benchmark that ... cases which we found in the loop invariant bibliography, and interfaces with three analysis programs...

two loop amplitudes
 Referenced in 7 articles
[sw25063]
 Local integrand representations of all twoloop amplitudes in planar SYM. We use generalized unitarity ... local, manifestly dualconformally invariant formulae for all twoloop scattering amplitudes in planar, maximally...

Aligator.jl
 Referenced in 1 article
[sw26257]
 Aligator.jl  a Julia package for loop invariant generation. We describe the Aligator.jl software package ... polynomial invariants of the rich class of extended Psolvable loops with nested conditionals. Aligator.jl ... form solutions of loop variables and infer the ideal of polynomial invariants by variable elimination...

Ultimate Taipan
 Referenced in 1 article
[sw28629]
 correct, they are guaranteed to be loop invariants for the path program. If they...

dypro
 Referenced in 1 article
[sw28851]
 particular given a task of recognizing loop invariants, we show dypro beats all static models...

Optgame
 Referenced in 6 articles
[sw04936]
 nonlinear timeinvariant system. OPTGAME 1.0 delivers openloop and feedback Nash equilibrium solutions, open...

$Apart
 Referenced in 5 articles
[sw10218]
 useful when one tries to perform loop calculations using packages such as Fire and Reduze ... integration by parts (IBP) identities and Lorentz invariance (LI) identities. A description ... FeynArts, and FeynCalc packages, to do oneloop calculations in double quarkonium production...

RGIsearch
 Referenced in 1 article
[sw17649]
 supports the computation of invariants up to twoloop level. A manual for the program...

QuIt
 Referenced in 1 article
[sw29333]
 express both functional and temporal properties of loops. We prove soundness and completeness ... termination analysis and invariant generation. For doing so, we express the loop semantics...

PackageX
 Referenced in 7 articles
[sw18225]
 package for the analytic computation of oneloop integrals dimensionally regulated near 4 spacetime dimensions ... kinematic configuration involving realvalued external invariants and internal masses. Output expressions can be readily ... computation of fermion form factors at oneloop. The package is intended to be used...

AODV
 Referenced in 4 articles
[sw29232]
 existing penandpaper proof of loop freedom of AODV. The protocol is modelled ... novel compositional approach for lifting invariants to networks of nodes. We exploit the mechanization...

SCOTS
 Referenced in 6 articles
[sw20172]
 algorithms to synthesize controllers with respect to invariance and reachability specifications. The atomic propositions, which ... Matlab interface to simulate the closed loop system and to visualize the abstract state space...

Aligators
 Referenced in 1 article
[sw09779]
 generation of universally quantified array invariants. Aligators leverages recurrence solving and algebraic techniques to carry ... inductive reasoning over array content. The Aligators’ loop extraction module allows treatment of multipath...