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

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

1 2 3 ... 28 29 30 next

  1. Chen, Mingshuai; Wang, Jian; An, Jie; Zhan, Bohua; Kapur, Deepak; Zhan, Naijun: NIL: learning nonlinear interpolants (2019)
  2. Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (2019)
  3. Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio: The Coq library as a theory graph (2019)
  4. Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
  5. Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Du, Hongwei: Verifying a scheduling protocol of safety-critical systems (2019)
  6. Cauderlier, Raphaël: Tactics and certificates in Meta Dedukti (2018)
  7. Derrick, John; Doherty, Simon; Dongol, Brijesh; Schellhorn, Gerhard; Travkin, Oleg; Wehrheim, Heike: Mechanized proofs of opacity: a comparison of two techniques (2018)
  8. Dubois, Catherine; Giorgetti, Alain: Tests and proofs for custom data generators (2018)
  9. He, Shaobo; Lahiri, Shuvendu K.; Rakamarić, Zvonimir: Verifying relative safety, accuracy, and termination for program approximations (2018)
  10. Lochbihler, Andreas: Fast machine words in Isabelle/HOL (2018)
  11. Lochbihler, Andreas; Schneider, Joshua: Relational parametricity and quotient preservation for modular (co)datatypes (2018)
  12. Moscato, Mariano M.; Lopez Pombo, Carlos G.; Muñoz, César A.; Feliú, Marco A.: Boosting the reuse of formal specifications (2018)
  13. Müller, Dennis; Kohlhase, Michael; Rabe, Florian: Automatically finding theory morphisms for knowledge management (2018)
  14. Müller, Dennis; Rabe, Florian; Kohlhase, Michael: Theories as types (2018)
  15. Petiot, Guillaume; Kosmatov, Nikolai; Botella, Bernard; Giorgetti, Alain; Julliand, Jacques: How testing helps to diagnose proof failures (2018)
  16. Rabe, Florian: A modular type reconstruction algorithm (2018)
  17. Shankar, Natarajan: Combining model checking and deduction (2018)
  18. 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)
  19. Zhang, Min; Ogata, Kazuhiro: From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories (2018)
  20. Aguado, F.; Ascariz, P.; Cabalar, P.; Pérez, G.; Vidal, C.: Verification for ASP denotational semantics: a case study using the PVS theorem prover (2017)

1 2 3 ... 28 29 30 next