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

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

1 2 3 ... 25 26 27 next

  1. He, Shaobo; Lahiri, Shuvendu K.; Rakamarić, Zvonimir: Verifying relative safety, accuracy, and termination for program approximations (2018)
  2. 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)
  3. Sardar, Muhammad Usama; Afaq, Nida; Hasan, Osman; Hoque, Khaza Anuarul: Towards probabilistic formal analysis of SATS-simultaneously moving aircraft (SATS-SMA) (2018)
  4. Zhang, Min; Ogata, Kazuhiro: From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories (2018)
  5. 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)
  6. 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)
  7. 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)
  8. Benzmüller, C.; Weber, Leon; Woltzenlogel Paleo, Bruno: Computer-assisted analysis of the Anderson-Hájek ontological controversy (2017)
  9. Berger, Ulrich; Hou, Tie: A realizability interpretation of Church’s simple theory of types (2017)
  10. Butterfield, Andrew: Utpcalc -- a calculator for UTP predicates (2017)
  11. Ferrari, Mauro; Fiorentini, Camillo; Fiorino, Guido: JTabWb: a Java framework for implementing terminating sequent and tableau calculi (2017)
  12. Gilbert, Frédéric: Proof certificates in PVS (2017)
  13. Jha, Susmit; Seshia, Sanjit A.: A theory of formal synthesis via inductive learning (2017)
  14. Kanckos, Annika; Woltzenlogel Paleo, B.: Variants of Gödel’s ontological proof in a natural deduction calculus (2017)
  15. Kohlhase, Michael; Müller, Dennis; Owre, Sam; Rabe, Florian: Making PVS accessible to generic services by interpretation in a universal format (2017)
  16. Lampropoulos, Leonidas; Gallois-Wong, Diane; Hriţcu, Cătălin; Hughes, John; Pierce, Benjamin C.; Xia, Li-yao: Beginner’s Luck: a language for property-based generators (2017)
  17. Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian: Classification of alignments between concepts of formal mathematical systems (2017)
  18. Nagashima, Yutaka; Kumar, Ramana: A proof strategy language and proof script generation for Isabelle/HOL (2017)
  19. Rocha, Camilo; Meseguer, José; Muñoz, César: Rewriting modulo SMT and open system analysis (2017)
  20. Bernardeschi, Cinzia; Domenici, Andrea: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (2016)

1 2 3 ... 25 26 27 next