
VCC
 Referenced in 71 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...

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

CLN2INV
 Referenced in 1 article
[sw41069]
 CLN2INV: Learning Loop Invariants with Continuous Logic Networks. Program verification offers a framework for ensuring ... eliminating different classes of bugs. Inferring loop invariants is one of the main challenges behind ... novel neural architecture for automatically learning loop invariants directly from program execution traces. Unlike existing ... Satisfiability Modulo Theories (SMT) for loop invariants from program execution traces. We develop...

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

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

Code2Inv
 Referenced in 1 article
[sw41066]
 smallscale yet expressive instances: a loop invariant synthesizer for C programs, and a Constrained...

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

CoVEGI
 Referenced in 0 articles
[sw39828]
 invariant generation. Finding an adequate loop invariant is key to the success of a verification...

HCOUP
 Referenced in 2 articles
[sw40157]
 evaluated at oneloop level in a gauge invariant manner in these models. HCOUP...

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