PVS

PVS is a verification system: that is, a specification language integrated with support tools and a theorem prover. It is intended to capture the state-of-the-art in mechanized formal methods and to be sufficiently rugged that it can be used for significant applications. PVS is a research prototype: it evolves and improves as we develop or apply new capabilities, and as the stress of real use exposes new requirements.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 629 articles , 4 standard articles )

Showing results 1 to 20 of 629.
Sorted by year (citations)

1 2 3 ... 30 31 32 next

  1. Dutle, Aaron; Moscato, Mariano; Titolo, Laura; Muñoz, César; Anderson, Gregory; Bobot, François: Formal analysis of the compact position reporting algorithm (2021)
  2. Kohlhase, Michael; Rabe, Florian: Experiences from exporting major proof assistant libraries (2021)
  3. Steen, Alexander; Benzmüller, Christoph: Extensional higher-order paramodulation in Leo-III (2021)
  4. Xu, Runqing; Li, Liming; Zhan, Bohua: Verified interactive computation of definite integrals (2021)
  5. Kahl, Wolfram: Calculational relation-algebraic proofs in the teaching tool \textscCalcCheck (2020)
  6. Perez, Ivan; Goodloe, Alwyn E.: Fault-tolerant functional reactive programming (extended version) (2020)
  7. Sheng, Feng; Zhu, Huibiao; He, Jifeng; Yang, Zongyuan; Bowen, Jonathan P.: Theoretical and practical approaches to the denotational semantics for MDESL based on UTP (2020)
  8. Shi, Zhiping; Guan, Yong; Li, Ximeng: Formalization of complex analysis and matrix theory (2020)
  9. Zhao, Liang; Wang, Xiaobing; Shu, Xinfeng; Zhang, Nan: A sound and complete proof system for a unified temporal logic (2020)
  10. Apt, Krzysztof R.; Olderog, Ernst-Rüdiger: Fifty years of Hoare’s logic (2019)
  11. Chen, Mingshuai; Wang, Jian; An, Jie; Zhan, Bohua; Kapur, Deepak; Zhan, Naijun: NIL: learning nonlinear interpolants (2019)
  12. Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (2019)
  13. Moore, J. Strother: Milestones from the Pure Lisp Theorem Prover to ACL2 (2019)
  14. Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio: The Coq library as a theory graph (2019)
  15. Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
  16. Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Du, Hongwei: Verifying a scheduling protocol of safety-critical systems (2019)
  17. Avelar da Silva, Andréia B.; de Lima, Thaynara Arielly; Galdino, André Luiz: Formalizing ring theory in PVS (2018)
  18. Cauderlier, Raphaël: Tactics and certificates in Meta Dedukti (2018)
  19. Derrick, John; Doherty, Simon; Dongol, Brijesh; Schellhorn, Gerhard; Travkin, Oleg; Wehrheim, Heike: Mechanized proofs of opacity: a comparison of two techniques (2018)
  20. Drechsler, Rolf (ed.): Formal system verification. State-of the-art and future trends (2018)

1 2 3 ... 30 31 32 next