• PVS

  • Referenced in 545 articles [sw03484]
  • verification system: that is, a specification language integrated with support tools and a theorem prover ... state-of-the-art in mechanized formal methods and to be sufficiently rugged that...
  • CafeOBJ

  • Referenced in 152 articles [sw06232]
  • behavioral system verification. We report on a machine supported method for verifying safety properties...
  • UNITY

  • Referenced in 164 articles [sw13461]
  • coupled state transition systems. Mechanical methods for mapping the transition systems first into ... formal assertions, permitting formal verification of the transition systems, and second into an executable program...
  • SIFT

  • Referenced in 500 articles [sw16554]
  • Scale-Invariant Keypoints. This paper presents a method for extracting distinctive invariant features from images ... single object, and finally performing verification through least-squares solution for consistent pose parameters. This...
  • HOL-Boogie

  • Referenced in 14 articles [sw00409]
  • annotations in first-order logic.\parIts verification conditions -- constructed via a wp calculus from these ... combining automated and interactive proof methods for code-verification.\parWe will exploit our proof-environment ... memory and machine models underlying the verification method...
  • STeP

  • Referenced in 29 articles [sw17948]
  • temporal specification. Unlike most systems for temporal verification, STeP is not restricted to finite-state ... combines model checking with deductive methods to allow the verification of a broad class...
  • CMC

  • Referenced in 31 articles [sw12422]
  • completely different method compared to existing real-time verification tools (HYTECH, KRONOS, UPPAAL). After...
  • Exp.Open

  • Referenced in 9 articles [sw07702]
  • Order, Compositional, and On-The-Fly Verification Methods. It is desirable to integrate formal verification...
  • DISCOVERER

  • Referenced in 35 articles [sw07719]
  • advances in program verification indicate that various verification problems can be reduced to semi-algebraic ... real closed fields are the general method for those problems. But the general ... method usually has low efficiency for specific problems. To overcome the bottleneck of program verification ... combine special techniques with the general method. Based on the work of complete discrimination systems...
  • d/dt

  • Referenced in 35 articles [sw10314]
  • with uncertain input. The verification procedure is based on a method for overapproximating reachable sets...
  • Truth/SLC

  • Referenced in 8 articles [sw01623]
  • their implementation. Formal specification and verification methods are therefore becoming more and more popular, aiming ... view of the inherent complexity of formal methods it is desirable to provide the user ... particularly successful automated approach to verification, called model checking, in which one tries to prove...
  • APMC

  • Referenced in 25 articles [sw11483]
  • Symbolic model checking methods have been extended recently to the verification of probabilistic systems. However ... this paper, we propose an approximation method to verify quantitative properties on discrete Markov chains...
  • Atoment

  • Referenced in 3 articles [sw19057]
  • specific language of development for program verification methods. It is used in the multilanguage software ... rapid development and testing of verification methods. The easy-to-use specialized language allows ... user of the system to describe verification methods in a natural notation, verify algorithms ... their representations as necessary, share verification methods with other users and combine them. In this...
  • D-Finder

  • Referenced in 13 articles [sw00200]
  • Finder tool implements a compositional method for the verification of component-based systems described...
  • CTIGAR

  • Referenced in 4 articles [sw23310]
  • Abstraction-Refinement (CTIGAR). Typical CEGAR-based verification methods refine the abstract domain based on full...
  • HANNIBAL

  • Referenced in 8 articles [sw10071]
  • verification of combinational circuits, which is based on recursive learning. In particular, the described method ... many practical verification problems where such internal equivalencies exist. The presented method can also...
  • Benchmarks

  • Referenced in 22 articles [sw04612]
  • safety verification of non-linear hybrid systems. We start from a classical method that uses...
  • PPL

  • Referenced in 80 articles [sw05357]
  • several systems for the analysis and verification of hardware and software components. Current applications span ... played an important role in the formal methods community and several critical tasks rely...
  • Minlog

  • Referenced in 10 articles [sw09765]
  • which implements proof-theoretic methods and applies them to verification and program extraction. We give...
  • JCML

  • Referenced in 2 articles [sw06406]
  • Java Card applets concentrates on static verification methods. This work presents a runtime verification approach...