• PVS

  • Referenced in 634 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...
  • KeY

  • Referenced in 65 articles [sw09969]
  • integrate design, implementation, formal specification, and formal verification of object-oriented software as seamlessly...
  • UNITY

  • Referenced in 185 articles [sw13461]
  • methodology starts with a simulation model specification in the form of a set of coupled ... first into a set of formal assertions, permitting formal verification of the transition systems ... formally that the model should obey and prove them as theorems using the formal specification...
  • seL4

  • Referenced in 91 articles [sw15222]
  • formal, machine-checked verification of the seL4 microkernel from an abstract specification down ... used a unique design approach that fuses formal and operating systems techniques. To our knowledge...
  • MAYA

  • Referenced in 26 articles [sw03423]
  • formal specifications usually reveals hidden errors causing the change of parts of the specification. Also ... changes of the specification which always endangers the verification work already done. In this paper ... structured specifications, which enables the use of various (structured) specification languages to formalize the software ... proof obligations arising from the specification, i.e. to perform verification in-the-small...
  • LTSA-WS

  • Referenced in 14 articles [sw10585]
  • performed. By providing early design verification and validation, the implementation, testing and deployment ... environment providing cooperating tools for specification, formal modeling, verification and validation of the composition process...
  • Why3

  • Referenced in 136 articles [sw04438]
  • verification. It provides a rich language for specification and programming, called WhyML, and relies ... provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library ... used as an intermediate language for the verification of C, Java, or Ada programs. Why3 ... user a possibility to easily reuse Why3 formalizations or to add support...
  • Truth/SLC

  • Referenced in 8 articles [sw01623]
  • Truth/SLC -- a parallel verification platform for concurrent systems. Concurrent software and hardware systems play ... correctness of their implementation. Formal specification and verification methods are therefore becoming more and more ... view of the inherent complexity of formal methods it is desirable to provide the user...
  • MCMAS

  • Referenced in 82 articles [sw09463]
  • MCMAS: A Model Checker for the Verification of Multi-Agent Systems. While temporal logic ... considering high-level agents attitudes. In particular, specification languages based on epistemic logic ... security specifications involving anonymity [4] are known to be naturally expressible in epistemic formalisms...
  • WSAT

  • Referenced in 37 articles [sw01022]
  • formal specification of web service composition. (2) Asynchronous messaging makes most interesting verification problems undecidable...
  • STeP

  • Referenced in 36 articles [sw17948]
  • formal verification of reactive, real-time and hybrid systems based on their temporal specification. Unlike...
  • RT-ASLAN

  • Referenced in 6 articles [sw30491]
  • advantages and disadvantages of formal specification and verification are included...
  • FoCs

  • Referenced in 20 articles [sw01591]
  • automatic generation of simulation checkers from formal specifications. For the foreseeable future, industrial hardware design ... simulation and model checking in the design verification process. To date, these techniques are applied ... individual advantages of simulation and formal verification...
  • CVT

  • Referenced in 17 articles [sw09952]
  • code validation tool (CVT). Automatic verification of a compilation process. We describe CVT -- a fully ... source specification. This approach is a viable alternative to a full formal verification ... freezing” the code generator design after verification. CVT was developed in the context ... validates the translation from StateMate/Sildex mixed specification into C. The use of novel techniques based...
  • SAEPTUM

  • Referenced in 2 articles [sw28617]
  • SAEPTUM: verification of ELAN hardware specifications using the proof assistant PVS. Rewriting and Rewriting-Logic ... been used in several applications, including specification, formal verification and construction of proof assistants. Previous ... works explored hardware specification and modeling using the rewriting-logic system ELA. Experiences proved this ... tool for formal verification of the correctness of the given hardware specifications. Although simple, verification...
  • LOTOSphere

  • Referenced in 9 articles [sw14748]
  • vehicle for efficient, yet formally based industrial software specification, design, verification, implementation and testing. LOTOSphere ... comprehensive treatment of the use of these formal description techniques in a software engineering environment...
  • qGCL

  • Referenced in 26 articles [sw39240]
  • formal semantics and body of laws, and provides a refinement calculus supporting the verification ... derivation of programs against their specifications. A representative selection of quantum algorithms are expressed...
  • VERSA

  • Referenced in 2 articles [sw21393]
  • Terms Real-time systems, process algebras, specification, verification, formal description techniques, resources, priority, software engineering...
  • Cadence SMV

  • Referenced in 27 articles [sw07795]
  • possible input sequences. While formal verification is often equated with equivalence checking, model checking ... allows you to verify that that your specifications are correct very early in the design...
  • ANNA

  • Referenced in 10 articles [sw36323]
  • features that are widely used in the specification and documentation of programs. 3. ANNA should ... within which the various established theories of formally specifying programs may be applied ... testing, debugging and formal verification of a finished program, but also specification of program parts...