• PVS

  • Referenced in 474 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 84 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 7 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...
  • 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 154 articles [sw00060]
  • ACL2 is both a programming language in which...
  • Coq

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

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

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

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

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

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

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

  • Referenced in 32 articles [sw01346]
  • Clean is a functional language based on Term...