• PVS

  • Referenced in 483 articles [sw03484]
  • PVS is a verification system: that is, a specification language integrated with support tools ... used for significant applications. PVS is a research prototype: it evolves and improves...
  • Isar

  • Referenced in 92 articles [sw04599]
  • semi-automated reasoning systems include Coq, PVS, HOL, and Isabelle. Despite this success in actually...
  • CCSL

  • Referenced in 19 articles [sw03357]
  • specifications into higher-order logic either for PVS or for for Isabelle/HOL (in new style...
  • TLPVS

  • Referenced in 8 articles [sw10024]
  • tlpvs: A pvs-Based ltl Verification System. In this paper we present our pvs implementation...
  • VSDITLU

  • Referenced in 8 articles [sw08725]
  • about the reals in the theorem prover PVS to aid in the transformation...
  • SAL

  • Referenced in 8 articles [sw13318]
  • includes many of the attractive features of PVS. The SAL toolkit provides several tools...
  • PVSio

  • Referenced in 3 articles [sw12428]
  • PVSio is a PVS package that extends the ground evaluator with a predefined library ... semantic attachments. PVSio has been part of PVS since PVS 5.0. The current version ... PVSio is 6.0 and is included in PVS 6.0. PVSio 6.0 provides: A standard library ... safely integrate the ground evaluator into the PVS theorem prover. These proof rules...
  • DisCo

  • Referenced in 6 articles [sw10393]
  • prototype verification back-end based on the PVS theorem prover also exists, and a model...
  • PVSio-web

  • Referenced in 2 articles [sw11949]
  • rapid prototyping device user interfaces in PVS. We present PVSio-web which extends the simulation ... component of the PVS proof system with functionalities for rapid prototyping device user interfaces ... experts in formal methods from using PVS. Designers load a picture of the layout ... layout, and link them to a PVS specification. They can then explore the behaviour...
  • LIRA

  • Referenced in 4 articles [sw21270]
  • first-order logic. Interactive theorem provers like pvs also make use of such decision procedures...
  • Manip

  • Referenced in 2 articles [sw12425]
  • manipulations for an interactive prover such as PVS can be labor intensive. We provide...
  • Dynamite 2.0

  • Referenced in 1 article [sw01320]
  • certainty provided by the theorem prover PVS. Using the Alloy Analyzer during the proving process ... improves the PVS theorem proving experience by reducing the number of errors introduced along creative...
  • ACL2

  • Referenced in 155 articles [sw00060]
  • ACL2 is both a programming language in which...
  • Coq

  • Referenced in 1159 articles [sw00161]
  • Coq is a formal proof management system. It...
  • Isabelle

  • Referenced in 393 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • Maple

  • Referenced in 3967 articles [sw00545]
  • The result of over 30 years of cutting...
  • Matlab

  • Referenced in 7110 articles [sw00558]
  • MATLAB® is a high-level language and interactive...
  • MetiTarski

  • Referenced in 30 articles [sw00573]
  • Many inequalities involving the functions ln, exp, sin...
  • QEPCAD

  • Referenced in 221 articles [sw00752]
  • QEPCAD B: A program for computing with semi...
  • Zing

  • Referenced in 37 articles [sw01037]
  • Zing is a software model checking project at...