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.


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

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

1 2 3 ... 29 30 31 next

  1. Kahl, Wolfram: Calculational relation-algebraic proofs in the teaching tool \textscCalcCheck (2020)
  2. Perez, Ivan; Goodloe, Alwyn E.: Fault-tolerant functional reactive programming (extended version) (2020)
  3. 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)
  4. Shi, Zhiping; Guan, Yong; Li, Ximeng: Formalization of complex analysis and matrix theory (2020)
  5. Zhao, Liang; Wang, Xiaobing; Shu, Xinfeng; Zhang, Nan: A sound and complete proof system for a unified temporal logic (2020)
  6. Apt, Krzysztof R.; Olderog, Ernst-Rüdiger: Fifty years of Hoare’s logic (2019)
  7. Chen, Mingshuai; Wang, Jian; An, Jie; Zhan, Bohua; Kapur, Deepak; Zhan, Naijun: NIL: learning nonlinear interpolants (2019)
  8. Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (2019)
  9. Moore, J. Strother: Milestones from the Pure Lisp Theorem Prover to ACL2 (2019)
  10. Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio: The Coq library as a theory graph (2019)
  11. Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
  12. Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Du, Hongwei: Verifying a scheduling protocol of safety-critical systems (2019)
  13. Avelar da Silva, Andréia B.; de Lima, Thaynara Arielly; Galdino, André Luiz: Formalizing ring theory in PVS (2018)
  14. Cauderlier, Raphaël: Tactics and certificates in Meta Dedukti (2018)
  15. Derrick, John; Doherty, Simon; Dongol, Brijesh; Schellhorn, Gerhard; Travkin, Oleg; Wehrheim, Heike: Mechanized proofs of opacity: a comparison of two techniques (2018)
  16. Dubois, Catherine; Giorgetti, Alain: Tests and proofs for custom data generators (2018)
  17. He, Shaobo; Lahiri, Shuvendu K.; Rakamarić, Zvonimir: Verifying relative safety, accuracy, and termination for program approximations (2018)
  18. Lochbihler, Andreas: Fast machine words in Isabelle/HOL (2018)
  19. Lochbihler, Andreas; Schneider, Joshua: Relational parametricity and quotient preservation for modular (co)datatypes (2018)
  20. Moscato, Mariano M.; Lopez Pombo, Carlos G.; Muñoz, César A.; Feliú, Marco A.: Boosting the reuse of formal specifications (2018)

1 2 3 ... 29 30 31 next