
PRISM
 Referenced in 390 articles
[sw01186]
 BDDs (binary decision diagrams) and MTBDDs (multiterminal BDDs); one based on sparse matrices ... been successfully used to analyse probabilistic termination, performance, and quality of service properties...

ode23
 Referenced in 247 articles
[sw06600]
 specify whether the integration is to terminate at a zero and whether the direction ... integration is to terminate at a zero of this event function and 0 otherwise. direction...

AProVE
 Referenced in 142 articles
[sw07831]
 AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework. AProVE ... most powerful systems for automated termination proofs of term rewrite systems (TRSs ... permits a completely flexible combination of different termination proof techniques. Due to this framework, AProVE ... also the first termination prover which can be fully configured by the user...

Walksat
 Referenced in 202 articles
[sw04328]
 assignment satisfies all clauses, the algorithm terminates, returning the assignment. Otherwise, a variable is flipped...

ASSAT
 Referenced in 160 articles
[sw02524]
 model M (terminates with failure if no such M exists). If M is an answer...

Tyrolean
 Referenced in 88 articles
[sw07830]
 Tyrolean Termination Tool 2 (TTT2) is a tool for automatically proving (and disproving) termination ... completely redesigned successor of TTT. Current (non)termination techniques include: approximated dependency graph, argument filtering...

REVE
 Referenced in 68 articles
[sw28907]
 described. REVE builds confluent and uniformly terminating term rewriting systems from sets of equations. Particular ... emphasis is placed on mechanization of termination proof. Indeed, REVE ... which can actually be called automatic because termination is fully integrated into the algorithms. REVE ... uses an incremental termination method based on recursive decomposition ordering which constructs the termination proof...

tn
 Referenced in 117 articles
[sw05140]
 truncated Newton method is to terminate the iterations earlier. A preconditioned truncated Newton method...

Pesca
 Referenced in 116 articles
[sw13664]
 Pesca can both be seen on the terminal and printed into LaTeX files. The user...

Find
 Referenced in 80 articles
[sw21614]
 intrusion of logical errors. The proof of termination is treated as a separate exercise. Finally...

CeTA
 Referenced in 40 articles
[sw06584]
 Certification of termination proofs using CeTA. There are many automatic tools to prove termination ... tools use a combination of many complex termination criteria. Hence generated proofs ... theorem prover Isabelle/HOL to automatically certify termination proofs. To this end, we first formalized ... theory of term rewriting including three major termination criteria: dependency pairs, dependency graphs, and reduction...

DART
 Referenced in 68 articles
[sw07260]
 program crashes, assertion violations, and nontermination. Preliminary experiments to unit test several examples...

CoLoR
 Referenced in 37 articles
[sw09806]
 application to the automated verifications of termination certificates. Termination is an important property of programs ... developed to address the problem of deciding termination for specific problems (since it is undecidable ... application to the automated verification of termination certificates, as produced by termination tools...

CiME
 Referenced in 38 articles
[sw09970]
 Enno Ohlebusch at Bielefeld university for termination of logic programs; the MUTERM tool ... www.dsic.upv.es/ slucas/csr/termination/muterm/ ) for termination of contextsensitive rewriting; the CARIBOO tool (developed at INRIA Nancy ... GrandEst) for termination of rewriting under strategies; and the MTT tool (http://www.lcc.uma.es/ duran/MTT ... termination of Maude programs. CiME2 is no longer maintained, and the currently developed version...

MUTERM
 Referenced in 34 articles
[sw10015]
 term: A Tool for Proving Termination of ContextSensitive Rewriting. Restrictions of rewriting can eventually ... achieve termination by pruning all infinite rewrite sequences issued from every term. Contextsensitive rewriting ... which can be used to automatically prove termination of CSR. The tool implements the generation ... appropriate orderings for proving termination of CSR by means of polynomial interpretations over the rational...

Dafny
 Referenced in 60 articles
[sw00183]
 frame specifications (read and write sets), and termination metrics. To further support specifications, the language...

LSMR
 Referenced in 55 articles
[sw12940]
 monotonic) it is safer to terminate LSMR early. We also report some experiments with reorthogonalization...

SPDE
 Referenced in 39 articles
[sw16714]
 used interactively on a computer terminal. In many cases the determining system is solved completely ... input information for the solution algorithm to terminate. The package should only be used...

VeriFast
 Referenced in 54 articles
[sw07705]
 algorithm is described that prevents nontermination of the SMT solver while enabling reduction...