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

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

1 2 3 ... 27 28 29 next

  1. Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (2019)
  2. Derrick, John; Doherty, Simon; Dongol, Brijesh; Schellhorn, Gerhard; Travkin, Oleg; Wehrheim, Heike: Mechanized proofs of opacity: a comparison of two techniques (2018)
  3. Dubois, Catherine; Giorgetti, Alain: Tests and proofs for custom data generators (2018)
  4. He, Shaobo; Lahiri, Shuvendu K.; Rakamarić, Zvonimir: Verifying relative safety, accuracy, and termination for program approximations (2018)
  5. Lochbihler, Andreas: Fast machine words in Isabelle/HOL (2018)
  6. Lochbihler, Andreas; Schneider, Joshua: Relational parametricity and quotient preservation for modular (co)datatypes (2018)
  7. Müller, Dennis; Kohlhase, Michael; Rabe, Florian: Automatically finding theory morphisms for knowledge management (2018)
  8. Müller, Dennis; Rabe, Florian; Kohlhase, Michael: Theories as types (2018)
  9. Newell, Josh; Pang, Linna; Tremaine, David; Wassyng, Alan; Lawford, Mark: Translation of IEC 61131-3 function block diagrams to PVS for formal verification with real-time nuclear application (2018)
  10. Petiot, Guillaume; Kosmatov, Nikolai; Botella, Bernard; Giorgetti, Alain; Julliand, Jacques: How testing helps to diagnose proof failures (2018)
  11. Rabe, Florian: A modular type reconstruction algorithm (2018)
  12. Sardar, Muhammad Usama; Afaq, Nida; Hasan, Osman; Hoque, Khaza Anuarul: Towards probabilistic formal analysis of SATS-simultaneously moving aircraft (SATS-SMA) (2018)
  13. Shankar, Natarajan: Combining model checking and deduction (2018)
  14. 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)
  15. Zhang, Min; Ogata, Kazuhiro: From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories (2018)
  16. 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)
  17. Aransay, Jesús; Divasón, Jose: A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (2017)
  18. Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington; Fernández, Maribel; Nantes-Sobrinho, Daniele: A formalisation of nominal (\alpha)-equivalence with A and AC function symbols (2017)
  19. Ayala-Rincón, Mauricio; de Moura, Flávio L. C.: Applied logic for computer scientists. Computational deduction and formal proofs (2017)
  20. Ayala-Rincón, Mauricio (ed.); Muñoz, César A. (ed.): Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26--29, 2017. Proceedings (2017)

1 2 3 ... 27 28 29 next