
PVS
 Referenced in 589 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 134 articles
[sw04599]
 semiautomated reasoning systems include Coq, PVS, HOL, and Isabelle. Despite this success in actually...

CCSL
 Referenced in 25 articles
[sw03357]
 specifications into higherorder 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 pvsBased ltl Verification System. In this paper we present our pvs implementation...

TAME
 Referenced in 5 articles
[sw28703]
 TAME: Using PVS strategies for specialpurpose 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 backend based on the PVS theorem prover also exists, and a model...

LIRA
 Referenced in 7 articles
[sw21270]
 firstorder logic. Interactive theorem provers like pvs also make use of such decision procedures...

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...

PVSioweb
 Referenced in 2 articles
[sw11949]
 rapid prototyping device user interfaces in PVS. We present PVSioweb 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 RewritingLogic 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...

MiniBrass
 Referenced in 1 article
[sw31298]
 algebraic framework of partially ordered valuation structures (PVS) that is implemented as an extension ... MiniSearch. We first demonstrate the adequacy of PVS to naturally augment partial orders with ... semiring from an arbitrary PVS. Both arguments draw upon elements from category theory. MiniBrass turns ... into practice: It offers a generic extensible PVS type system, reusable implementations of specific soft...

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...

clock synchronization
 Referenced in 1 article
[sw28680]
 using the theorem prover EHDM (precursor to PVS). Our formalization in Isabelle/HOL is based...

ACL2
 Referenced in 262 articles
[sw00060]
 ACL2 is both a programming language in which...

Coq
 Referenced in 1689 articles
[sw00161]
 Coq is a formal proof management system. It...