
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 Psolvability 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 networkwide 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 networkwide invariant violations dynamically as each forwarding...

Jass
 Referenced in 11 articles
[sw32265]
 technique that allows runtime 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 boundedtime 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 highlevel 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, postconditions, 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 redblack 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]
 objectoriented language with garbage collection, staticallychecked 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 ... infinitebounded model checkers can prove invariants by kinduction. SAL has been available since...

BoogiePL
 Referenced in 13 articles
[sw21521]
 BoogiePL: A typed procedural language for checking objectoriented 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 bitprecise 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 usersupplied Jacobians...