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