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

Aligator
 Referenced in 10 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...

two loop amplitudes
 Referenced in 25 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...

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

Aligator.jl
 Referenced in 3 articles
[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...

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

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

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

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

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

SCOTS
 Referenced in 15 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...

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

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

EFTofPNG
 Referenced in 5 articles
[sw20815]
 full computation of all derivatives and gauge invariant physical observables of interest. The upcoming ”EFTofPNG ... fourth PN order, and the twoloop level. We expect and strongly encourage public development...