• DISCOVERER

  • Referenced in 55 articles [sw07719]
  • this direction, including SAS-solving itself, termination analysis and invariant generation of programs, and reachability...
  • PRISM

  • Referenced in 416 articles [sw01186]
  • decision processes and continuous-time Markov chains. Analysis is performed through model checking such systems ... BDDs (binary decision diagrams) and MTBDDs (multi-terminal BDDs); one based on sparse matrices...
  • CSI

  • Referenced in 22 articles [sw09767]
  • combined flexibly. Methods developed for termination analysis are adapted to prove and disprove confluence. Preliminary...
  • FLATA

  • Referenced in 18 articles [sw04142]
  • error control state is reachable termination analysis of non-recursive programs - computation of termination preconditions...
  • KITTeL

  • Referenced in 8 articles [sw17045]
  • Termination analysis of C programs using compiler intermediate languages. Modeling the semantics of programming languages ... like C for the automated termination analysis of programs is a challenge if complete coverage ... these intermediate languages for the automated termination analysis of C programs. In this paper ... into term rewrite systems (TRSs), and the termination proof itself is then performed...
  • VMTL

  • Referenced in 8 articles [sw10065]
  • modular termination laboratory. The automated analysis of termination of term rewriting systems (TRSs) has drawn ... most recent and powerful algorithms for termination analysis of TRSs, while providing an open interface ... modular extensibility, VMTL focuses on analyzing the termination behaviour of conditional term rewriting systems (CTRSs...
  • TyPiCal

  • Referenced in 8 articles [sw23207]
  • code elimination, information flow analysis, and termination analysis. The former two analyses aim to statically...
  • PAG

  • Referenced in 19 articles [sw00669]
  • theories of abstract interpretation and data flow analysis the implementation and design of analyzers ... derivation of provably correct and terminating analyses. Data flow analysis supplies many efficient algorithms, such...
  • Terminyzer

  • Referenced in 4 articles [sw08335]
  • There have been many studies on termination analysis of logic programs but little has been ... important task, in our opinion. Non-termination analysis examines program execution history when non-termination ... user. Terminyzer includes several non-termination analysis approaches of different computational complexity. These approaches ... calls that are likely causes of non-terminating cycles. It also provides the sequences...
  • TALP

  • Referenced in 5 articles [sw00946]
  • TALP: A tool for the termination analysis of logic programs...
  • COSTA

  • Referenced in 23 articles [sw00162]
  • automatic program analysis and which is able to infer cost and termination information about Java ... executed by the program. When performing cost analysis, COSTA produces a cost equation system, which ... upper bounds on cost as for proving termination (which also implies the boundedness ... range of possibilities which differ in the analysis accuracy and overhead. All this, without requiring...
  • IsaFoL

  • Referenced in 4 articles [sw19193]
  • Isabelle/HOL Formalization of Rewriting for Certified Termination Analysis) at Universität Innsbruck...
  • TERMINATOR

  • Referenced in 3 articles [sw06692]
  • Symbolic termination analysis of solvable loops. Termination is an essential part of program correctness...
  • EMP

  • Referenced in 8 articles [sw01086]
  • rule-based error analysis in case of nonsuccessful termination...
  • DART

  • Referenced in 71 articles [sw07260]
  • program can operate in; and (3) dynamic analysis of how the program behaves under random ... program crashes, assertion violations, and non-termination. Preliminary experiments to unit test several examples...
  • UPPAAL TIGA

  • Referenced in 42 articles [sw12913]
  • truly on-the-fly algorithms for their analysis. The algorithm we propose [CDFLL05 ... symbolic algorithm may terminate long before having explored the entire state-space. Also the individual...
  • QuIt

  • Referenced in 1 article [sw29333]
  • Loop analysis by quantification over iterations. We present a framework to analyze and verify programs ... tasks of partial correctness verification, termination analysis and invariant generation. For doing so, we express...
  • CyNTHIA

  • Referenced in 1 article [sw19663]
  • behaviour, e.g., whether it is terminating. All analysis is done using the Oyster system, which...
  • SAS4A

  • Referenced in 1 article [sw12523]
  • fuel melting and relocation. SAS4A analysis is terminated upon loss of subassembly hexcan integrity...
  • A3PAT

  • Referenced in 8 articles [sw21587]
  • known in the literature, thus yielding new termination criteria, such as an extension ... improve on previous works on formalisation and analysis of dependency graphs...