• BLAST

  • Referenced in 124 articles [sw02937]
  • Abstraction Software verification Tool) is a static software verification tool for C language that solves...
  • Dafny

  • Referenced in 62 articles [sw00183]
  • language is designed to support the static verification of programs. It is imperative, sequential, supports ... ghost constructs are used only during verification; the compiler omits them from the executable code.The ... same way as with the static type checker—when the tool produces errors, the programmer...
  • SLAM

  • Referenced in 150 articles [sw03136]
  • software that ensure reliable and correct functioning. Static Driver Verifier is a tool ... Driver Development Kit that uses the SLAM verification engine...
  • CiaoPP

  • Referenced in 41 articles [sw12089]
  • program, etc. Certain kinds of static debugging and verification, finding errors before running the program...
  • DyTa

  • Referenced in 3 articles [sw22848]
  • DyTa: dynamic symbolic execution guided with static verification results. Software-defect detection is an increasingly ... detect defects in a program, static verification and dynamic test generation are two important proposed ... these techniques face their respective issues. Static verification produces false positives, and on the other ... consuming. To address the limitations of static verification and dynamic test generation, we present...
  • WhyML

  • Referenced in 24 articles [sw09709]
  • provers. To keep verification conditions tractable and comprehensible, WhyML imposes a static control of aliases ... used as an intermediate language for the verification of C, Java, or Ada programs...
  • GraVy

  • Referenced in 2 articles [sw34340]
  • Gradual Verifier. Static verification traditionally produces yes/no answers. It either provides a proof that ... violated. Hence, the progress of static verification is hard to measure. Unlike in testing, where ... used to track progress, static verification does not provide any intermediate result until the proof ... incompleteness of static verifiers. To overcome this, we propose a gradual verification approach, GraVy...
  • HALO

  • Referenced in 3 articles [sw23942]
  • useful post-condition. We study the static verification of such contracts. Our main contribution...
  • JCML

  • Referenced in 2 articles [sw06406]
  • impose the use of dynamic, on-card verifications, but most of the research developed ... Java Card applets concentrates on static verification methods. This work presents a runtime verification approach...
  • YOGI

  • Referenced in 12 articles [sw13094]
  • combining static analysis and testing. Yogi implements the Dash algorithm which performs verification by combining ... that it plugs into Microsoft’s Static Driver Verifier framework. We have used this framework...
  • ESC4

  • Referenced in 2 articles [sw07219]
  • modeling language Extended Static Checking (ESC) is a fully automated formal verification technique. Verification ... translating programs and their specifications into verification conditions (VCs). Proof of a VC establishes ... beyond the ability of traditional extended static checking tools to verify. Not being able ... that lies between ESC and full static program verification. ESC is generally quite efficient...
  • Cibai

  • Referenced in 4 articles [sw26821]
  • abstract interpretation-based static analyzer for modular analysis and verification of Java classes. We introduce ... generic static analyzer based on abstract interpretation for the modular analysis and verification of Java...
  • BicolanoMT

  • Referenced in 3 articles [sw28593]
  • developed to be suited for program verification and static analysis...
  • COMBINE

  • Referenced in 1 article [sw01423]
  • COMBINE (Combined fOrmal Methods for BINdingly vErification). Suggested by its name, COMBINE can verify imperative ... bindingly manner comprising of two phases: static verification and dynamic verification. In fact, COMBINE...
  • Jerboa

  • Referenced in 1 article [sw10051]
  • modeler editor is equipped with many static verification mechanisms that ensure that the generated modelers...
  • Verigraph

  • Referenced in 4 articles [sw23736]
  • rule-based framework, suitable for modelling both static and dynamic aspects of complex systems ... algebraic GT which underlies verification techniques such as static analysis. Current tools based...
  • CodeContracts

  • Referenced in 2 articles [sw30949]
  • improve testing via runtime checking, enable static contract verification, and documentation generation. Code Contracts bring...
  • Jahob

  • Referenced in 10 articles [sw12385]
  • verification system for programs written in a subset of Java. Using Jahob, developers can statically...
  • Omnibus

  • Referenced in 3 articles [sw04600]
  • time assertion checking, extended static checking and full formal verification. The language is supported...
  • Clousot

  • Referenced in 1 article [sw13331]
  • locals). Without such an analysis, static symbolic verification is unsound and hence may report false...