• 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 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...
  • two loop amplitudes

  • Referenced in 25 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...
  • 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...
  • 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 P-solvable 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 loop-invariant 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]
  • small-scale 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 time-invariant system. OPTGAME 1.0 delivers open-loop 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 one-loop 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...
  • H-COUP

  • Referenced in 2 articles [sw40157]
  • evaluated at one-loop level in a gauge invariant manner in these models. H-COUP...
  • Package-X

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