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 602 articles , 4 standard articles )

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

1 2 3 ... 29 30 31 next

  1. Apt, Krzysztof R.; Olderog, Ernst-Rüdiger: Fifty years of Hoare’s logic (2019)
  2. Chen, Mingshuai; Wang, Jian; An, Jie; Zhan, Bohua; Kapur, Deepak; Zhan, Naijun: NIL: learning nonlinear interpolants (2019)
  3. Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (2019)
  4. Moore, J. Strother: Milestones from the Pure Lisp Theorem Prover to ACL2 (2019)
  5. Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio: The Coq library as a theory graph (2019)
  6. Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
  7. Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Du, Hongwei: Verifying a scheduling protocol of safety-critical systems (2019)
  8. Cauderlier, Raphaël: Tactics and certificates in Meta Dedukti (2018)
  9. Derrick, John; Doherty, Simon; Dongol, Brijesh; Schellhorn, Gerhard; Travkin, Oleg; Wehrheim, Heike: Mechanized proofs of opacity: a comparison of two techniques (2018)
  10. Dubois, Catherine; Giorgetti, Alain: Tests and proofs for custom data generators (2018)
  11. He, Shaobo; Lahiri, Shuvendu K.; Rakamarić, Zvonimir: Verifying relative safety, accuracy, and termination for program approximations (2018)
  12. Lochbihler, Andreas: Fast machine words in Isabelle/HOL (2018)
  13. Lochbihler, Andreas; Schneider, Joshua: Relational parametricity and quotient preservation for modular (co)datatypes (2018)
  14. Moscato, Mariano M.; Lopez Pombo, Carlos G.; Muñoz, César A.; Feliú, Marco A.: Boosting the reuse of formal specifications (2018)
  15. Müller, Dennis; Kohlhase, Michael; Rabe, Florian: Automatically finding theory morphisms for knowledge management (2018)
  16. Müller, Dennis; Rabe, Florian; Kohlhase, Michael: Theories as types (2018)
  17. Petiot, Guillaume; Kosmatov, Nikolai; Botella, Bernard; Giorgetti, Alain; Julliand, Jacques: How testing helps to diagnose proof failures (2018)
  18. Rabe, Florian: A modular type reconstruction algorithm (2018)
  19. Shankar, Natarajan: Combining model checking and deduction (2018)
  20. Shi, Ling; Zhao, Yongxin; Liu, Yang; Sun, Jun; Dong, Jin Song; Qin, Shengchao: A UTP semantics for communicating processes with shared variables and its formal encoding in PVS (2018)

1 2 3 ... 29 30 31 next