• Daikon

  • Referenced in 44 articles [sw04319]
  • invariant detector reports likely program invariants. An invariant is a property that holds ... Users can extend Daikon to check for additional invariants. Dynamic invariant detection runs a program ... easy to extend Daikon to other applications. Invariants can be useful in program understanding ... theorem proving, repairing inconsistent data structures, and checking the validity of data streams, among other...
  • c2i

  • Referenced in 6 articles [sw19488]
  • From invariant checking to invariant inference using randomized search. We describe a general framework ... invariant inference procedure from an invariant checking procedure. Given a checker and a language...
  • Aligator

  • Referenced in 10 articles [sw00029]
  • package Aligator for automatically inferring polynomial loop invariants. The package combines algorithms from symbolic summation ... solvable loops. Aligator contains routines for checking the P-solvability of loops, transforming them into ... polynomial invariants by variable elimination, invariant filtering and completeness check of the resulting...
  • Salsa

  • Referenced in 5 articles [sw25430]
  • constraint solvers with BDDs for automated invariant checking. Salsa is an invariant checker for specifications...
  • VeriFlow

  • Referenced in 6 articles [sw25229]
  • invariants in real time. Networks are complex and prone to bugs. Existing tools that check ... arise. Is it possible to check network-wide invariants in real time, as the network ... achieve extremely low latency during the checks so that network performance is not affected ... controller and network devices that checks for network-wide invariant violations dynamically as each forwarding...
  • Jass

  • Referenced in 11 articles [sw32265]
  • technique that allows run-time checks of specification violation and their treatment during program execution ... postconditions, invariants), Jass additionally supports refinement, i.e. subtyping,checks and the novel concept oftrace assertions...
  • C2e2

  • Referenced in 11 articles [sw20139]
  • Compare Execute Check Engine (C2E2) is a tool for verifying bounded-time invariant properties...
  • Wolverine

  • Referenced in 13 articles [sw14483]
  • interpolants. Wolverine is a software verifier that checks safety properties of sequential ANSI ... programs, deploying Craig interpolation to derive program invariants. We describe the underlying approach...
  • Anteater

  • Referenced in 4 articles [sw32373]
  • translates high-level network invariants into boolean satisfiability problems (SAT), checks them against network state...
  • One Optimal System

  • Referenced in 3 articles [sw24718]
  • invariants of Lie algebra in spite of Killing form checking possible constraints of each classification...
  • CodeContracts

  • Referenced in 2 articles [sw30949]
  • conditions, post-conditions, and object invariants. Contracts act as checked documentation of your external...
  • Stardust

  • Referenced in 1 article [sw20015]
  • legibly specify certain classes of program invariants that are verified at compile time. This ... apply both value refinements (to check red-black tree invariants) and invaluable refinements (to check...
  • MCUnit

  • Referenced in 1 article [sw36219]
  • chain has the correct invariant distribution. They do not check other properties of successful samplers...
  • Sather

  • Referenced in 8 articles [sw34049]
  • object-oriented language with garbage collection, statically-checked strong typing, multiple inheritance, separate implementations ... exception handling, assertions, preconditions, postconditions, and class invariants. Code can be compiled into C code...
  • SAL

  • Referenced in 9 articles [sw13318]
  • checker uses Yices to provide bounded model checking for systems defined over infinite data types ... infinite-bounded model checkers can prove invariants by k-induction. SAL has been available since...
  • BoogiePL

  • Referenced in 13 articles [sw21521]
  • BoogiePL: A typed procedural language for checking object-oriented programs. This note defines BoogiePL ... analyses such as the inference of program invariants. In this way, BoogiePL also serves...
  • FrankenBit

  • Referenced in 3 articles [sw25253]
  • Bounded Model Checking, proving bit-precise safety, i.e. synthesizing a safe inductive invariant, remains...
  • jContractor

  • Referenced in 10 articles [sw01488]
  • intuitive naming convention. Preconditions, postconditions, and invariants can be associated with, or inherited ... engineering technique allows it to specify and check contracts even when source code...
  • SBA

  • Referenced in 24 articles [sw05242]
  • License (GPL). Bundle Adjustment (BA) is almost invariably used as the last step of every ... finite differences. Additionally, sba includes routines for checking the consistency of user-supplied Jacobians...