• PVS

  • Referenced in 587 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 125 articles [sw04599]
  • semi-automated reasoning systems include Coq, PVS, HOL, and Isabelle. Despite this success in actually...
  • CCSL

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

  • Referenced in 10 articles [sw28648]
  • NASA PVS Library is a collection of formal developments in PVS maintained by the NASA ... Methods Team and is part of the PVS research sponsored by NASA Langley. The current...
  • TLPVS

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

  • Referenced in 5 articles [sw28703]
  • TAME: Using PVS strategies for special-purpose theorem proving. TAME (Timed Automata Modeling Environment ... interface to the theorem proving system PVS, is designed for proving properties of three classes ... auxiliary theories, and a set of specialized PVS strategies that rely on these theories ... understood without executing them in the PVS proof checker. Several new PVS features...
  • VSDITLU

  • Referenced in 9 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...
  • DisCo

  • Referenced in 7 articles [sw10393]
  • prototype verification back-end based on the PVS theorem prover also exists, and a model...
  • 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...
  • LIRA

  • Referenced in 6 articles [sw21270]
  • first-order logic. Interactive theorem provers like pvs also make use of such decision procedures...
  • 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...
  • SAEPTUM

  • Referenced in 2 articles [sw28617]
  • ELAN hardware specifications using the proof assistant PVS. Rewriting and Rewriting-Logic have been used ... translation to the proof assistant PVS and automatic generation of critical pair based correction criteria...
  • Ocsid

  • Referenced in 2 articles [sw28725]
  • structural embedding of Ocsid in PVS. We describe a structural embedding of the Ocsid specification ... language into the logic of the PVS theorem prover. A front end tool is used...
  • 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 256 articles [sw00060]
  • ACL2 is both a programming language in which...
  • Coq

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

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