A Brief Overview of PVS

DOI10.1007/978-3-540-71067-7_5MaRDI QIDQ3543645zbMATH OpenOpenAlexFDO

Authors Sam Owre, Natarajan Shankar

Publication date 4 December 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71067-7_5

Mathematics Subject Classification ID

Recommendations

• PVS\#: streamlined tacticals for PVS
• A Brief Overview of HOL4
• Computer Aided Verification
• scientific article; zbMATH DE number 1903374
• PVS strategies for proving abstraction properties of automata

Cites work

• scientific article; zbMATH DE number 1670737 (Why is no real title available?)
• scientific article; zbMATH DE number 1670802 (Why is no real title available?)
• scientific article; zbMATH DE number 1064116 (Why is no real title available?)
• scientific article; zbMATH DE number 2080050 (Why is no real title available?)
• scientific article; zbMATH DE number 1863375 (Why is no real title available?)
• scientific article; zbMATH DE number 2090113 (Why is no real title available?)
• TAME: Using PVS strategies for special-purpose theorem proving

Cited in

(11)

• PVS
• Recursive tables and effective definition schemes
• Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem
• Compositional reasoning using intervals and time reversal
• PVS\#: streamlined tacticals for PVS
• Validating QBF Validity in HOL4
• Proof normalization modulo
• The Implicit Calculus of Constructions as a Programming Language with Dependent Types
• Theorem prover approach to semistructured data design
• Proving the infeasibility of Horn formulas through read-once resolution
• Operations on fixpoint equation systems

Describes a project that uses

Uses Software

• TAME

This page was built for publication: A Brief Overview of PVS

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3543645)