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

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

1 2 3 ... 23 24 25 next

  1. 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)
  2. Benzmüller, C.; Weber, Leon; Woltzenlogel Paleo, Bruno: Computer-assisted analysis of the Anderson-Hájek ontological controversy (2017)
  3. Kanckos, Annika; Woltzenlogel Paleo, B.: Variants of Gödel’s ontological proof in a natural deduction calculus (2017)
  4. Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian: Classification of alignments between concepts of formal mathematical systems (2017)
  5. Nagashima, Yutaka; Kumar, Ramana: A proof strategy language and proof script generation for Isabelle/HOL (2017)
  6. Rocha, Camilo; Meseguer, José; Muñoz, César: Rewriting modulo SMT and open system analysis (2017)
  7. Bernardeschi, Cinzia; Domenici, Andrea: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (2016)
  8. Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Formalization of real analysis: a survey of proof assistants and libraries (2016)
  9. Carvalho, Gustavo; Cavalcanti, Ana; Sampaio, Augusto: Modelling timed reactive systems from natural-language requirements (2016)
  10. Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano: Infinite-state invariant checking with IC3 and predicate abstraction (2016)
  11. Halmagrand, Pierre: Soundly proving B method formulæusing typed sequent calculus (2016)
  12. Hesselink, Wim H.: Correctness and concurrent complexity of the black-white bakery algorithm (2016)
  13. John, Ajith K.; Chakraborty, Supratik: A layered algorithm for quantifier elimination from linear modular constraints (2016)
  14. Liu, Shaoying: Testing-based formal verification for theorems and its application in software specification verification (2016)
  15. Martin-Dorel, Érik; Melquiond, Guillaume: Proving tight bounds on univariate expressions with elementary functions in Coq (2016)
  16. Rabe, Florian: The future of logic: foundation-independence (2016)
  17. Rossi, Matteo; Mandrioli, Dino; Morzenti, Angelo; Ferrucci, Luca: A temporal logic for micro- and macro-step-based real-time systems: foundations and applications (2016)
  18. Wang, Timothy; Jobredeaux, Romain; Pantel, Marc; Garoche, Pierre-Loic; Feron, Eric; Henrion, Didier: Credible autocoding of convex optimization algorithms (2016)
  19. Wimmer, Simon: Formalized timed automata (2016)
  20. Zhan, Bohua: AUTO2, A saturation-based heuristic prover for higher-order logic (2016)

1 2 3 ... 23 24 25 next