• 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 P-solvable loops. Aligator contains routines for checking the P-solvability ... 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 non-trivial 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 loop-invariant 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 two-loop amplitudes in planar SYM. We use generalized unitarity ... local, manifestly dual-conformally invariant formulae for all two-loop 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 P-solvable 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 time-invariant system. OPTGAME 1.0 delivers open-loop 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 one-loop calculations in double quarkonium production...
  • RGIsearch

  • Referenced in 1 article [sw17649]
  • supports the computation of invariants up to two-loop 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...
  • Package-X

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

  • Referenced in 4 articles [sw29232]
  • existing pen-and-paper 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 multi-path...