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.

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

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

1 2 3 ... 30 31 32 next

  1. Baxter, James; Ribeiro, Pedro; Cavalcanti, Ana: Sound reasoning in \textittock-CSP (2022)
  2. Boldo, Sylvie; Clément, François; Faissole, Florian; Martin, Vincent; Mayero, Micaela: A Coq formalization of Lebesgue integration of nonnegative functions (2022)
  3. Hirata, Michikazu; Minamide, Yasuhiko; Sato, Tetsuya: Program logic for higher-order probabilistic programs in Isabelle/HOL (2022)
  4. Lewis, Robert Y.; Wu, Minchao: A bi-directional extensible interface between Lean and Mathematica (2022)
  5. de Lima, Thaynara Arielly; Galdino, André Luiz; Avelar, Andréia Borges; Ayala-Rincón, Mauricio: Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem (2021)
  6. Dutle, Aaron; Moscato, Mariano; Titolo, Laura; Muñoz, César; Anderson, Gregory; Bobot, François: Formal analysis of the compact position reporting algorithm (2021)
  7. Kohlhase, Michael; Rabe, Florian: Experiences from exporting major proof assistant libraries (2021)
  8. Melcer, Daniel; Chang, Stephen: ProofViz: an interactive visual proof explorer (2021)
  9. Rabe, Florian: A language with type-dependent equality (2021)
  10. Sogokon, Andrew; Mitsch, Stefan; Tan, Yong Kiam; Cordwell, Katherine; Platzer, André: Pegasus: sound continuous invariant generation (2021)
  11. Steen, Alexander; Benzmüller, Christoph: Extensional higher-order paramodulation in Leo-III (2021)
  12. Xu, Runqing; Li, Liming; Zhan, Bohua: Verified interactive computation of definite integrals (2021)
  13. Kahl, Wolfram: Calculational relation-algebraic proofs in the teaching tool \textscCalcCheck (2020)
  14. Perez, Ivan; Goodloe, Alwyn E.: Fault-tolerant functional reactive programming (extended version) (2020)
  15. 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)
  16. Shi, Zhiping; Guan, Yong; Li, Ximeng: Formalization of complex analysis and matrix theory (2020)
  17. Zhao, Liang; Wang, Xiaobing; Shu, Xinfeng; Zhang, Nan: A sound and complete proof system for a unified temporal logic (2020)
  18. Apt, Krzysztof R.; Olderog, Ernst-Rüdiger: Fifty years of Hoare’s logic (2019)
  19. Chen, Mingshuai; Wang, Jian; An, Jie; Zhan, Bohua; Kapur, Deepak; Zhan, Naijun: NIL: learning nonlinear interpolants (2019)
  20. Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (2019)

1 2 3 ... 30 31 32 next